diff options
| -rw-r--r-- | isa/Example.ML | 8 | ||||
| -rw-r--r-- | isa/Example.thy | 4 | ||||
| -rw-r--r-- | isa/Example2.ML | 12 |
3 files changed, 11 insertions, 13 deletions
diff --git a/isa/Example.ML b/isa/Example.ML index 49b6ee5a..4795d79f 100644 --- a/isa/Example.ML +++ b/isa/Example.ML @@ -2,7 +2,7 @@ Example proof script for Isabelle Proof General. $Id$ -*) +*) Goal "A & B --> B & A"; by (rtac impI 1); @@ -13,7 +13,5 @@ Goal "A & B --> B & A"; qed "and_comms"; Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)"; -by (blast_tac (claset()) 1); - - - + by (blast_tac (claset()) 1); +qed ""; diff --git a/isa/Example.thy b/isa/Example.thy index 84a71f31..252a5a4c 100644 --- a/isa/Example.thy +++ b/isa/Example.thy @@ -1,10 +1,10 @@ (* - Example theory file for Isabelle + Example theory file for Isabelle David Aspinall <da@dcs.ed.ac.uk> $Id$ -*) +*) Example = Main diff --git a/isa/Example2.ML b/isa/Example2.ML index 5d904930..ab2fef03 100644 --- a/isa/Example2.ML +++ b/isa/Example2.ML @@ -4,12 +4,12 @@ $Id$ Same as Example.ML, except using X-Symbol input tokens. -*) +*) Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; -by (rtac impI 1); -by (etac conjE 1); -by (rtac conjI 1); -by (assume_tac 1); -by (assume_tac 1); + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); qed "and_comms"; |