Email Gateway (Aug 22 2022 at 11:02): Email Gateway (Aug 22 2022 at 11:02):From: Holger Blasum <hbl@sysgo.com>
Dear Isabelle users,
let's say I have a proof written by somebody else, that is consisting
of two steps. If I want to see what Isabelle rules have been applied for a
single proof step how do I do it?
Example below: assume I simply want to see the rule(s) that have/has been
applied in step 2 without mixing them up with anything any rule
that has been applied in step 1.
theory test
imports Main
begin
lemma combined:
assumes a1: "ALL n::nat. A n --> B"
and a2: "B --> C"
shows "A 0 --> C"
proof-
(* step 1 *) from a1 and a2 have "ALL n. A n --> C" by blast
(* step 2 *) from this show "A 0 --> C" by auto
qed
end
Thanks and best,
Last updated: Apr 25 2024 at 20:15 UTC