diff options
author | Makarius Wenzel <makarius@sketis.net> | 1999-04-16 16:15:27 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 1999-04-16 16:15:27 +0000 |
commit | 9bafbd1b551c9cf8d7c3a7fb96511966ed094831 (patch) | |
tree | 05cbcb8b6ee845e4d77285ee6bf3d3cf9849b9c0 /isar/Example.thy | |
parent | 9d69d66256b4c88c89fb3903de29bc71b2fb36cb (diff) |
initial version of 'isar proof assistant (Isabelle/Isar);
Diffstat (limited to 'isar/Example.thy')
-rw-r--r-- | isar/Example.thy | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/isar/Example.thy b/isar/Example.thy new file mode 100644 index 00000000..b8b7328b --- /dev/null +++ b/isar/Example.thy @@ -0,0 +1,12 @@ + +theory Example = Main:; + +lemma "A --> B --> A"; +proof; + assume A; + show "B --> A"; + proof; + qed; +qed; + +end; |