diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 14:53:10 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 14:53:10 +0000 |
| commit | ea3e60264221ccd4bb880f1a30e157b420ca6e66 (patch) | |
| tree | 59626dbf78bdf4a47bd0afb58b49e805068005b2 /isar/Example.thy | |
| parent | f70acea9b01ebe800c3d7250fa8c5fb035cb846f (diff) | |
Remove comment about selecting PG/Isar.
Diffstat (limited to 'isar/Example.thy')
| -rw-r--r-- | isar/Example.thy | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 0d7edca7..fc72c2f7 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -1,12 +1,7 @@ -(* -*- isar -*- - +(* Example proof document for Isabelle/Isar Proof General. $Id$ - - The first line forces Isabelle/Isar Proof General, otherwise - you may get the theory mode of ordinary Isabelle Proof General - See the manual for other ways to select Isabelle/Isar PG. *) theory Example = Main: @@ -19,8 +14,9 @@ proof then show "B & A" proof assume B and A - then show ?thesis .. - qed + then + show ?thesis .. + qed qed |