diff options
Diffstat (limited to 'isar/Example.thy')
| -rw-r--r-- | isar/Example.thy | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 8dc4b04a..f9807888 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -1,6 +1,10 @@ theory Example = Main:; +text {* + Just a few tiny examples to get an idea of how Isabelle/Isar proof documents + may look like. + *} lemma I: "A --> A"; proof; @@ -17,6 +21,11 @@ proof; qed; qed; +text {* + This one is a good test for ProofGeneral to cope with block-structured + proof texts. Have fun with automatic indentation! + *}; + lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"; proof; assume "A --> B --> C"; |