diff options
Diffstat (limited to 'isar/Example.thy')
-rw-r--r-- | isar/Example.thy | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index b8b7328b..8dc4b04a 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -1,12 +1,39 @@ theory Example = Main:; -lemma "A --> B --> A"; + +lemma I: "A --> A"; +proof; + assume A; + show A; .; +qed; + +lemma K: "A --> B --> A"; proof; assume A; show "B --> A"; proof; + show A; .; qed; qed; +lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"; +proof; + assume "A --> B --> C"; + show "(A --> B) --> A --> C"; + proof; + assume "A --> B"; + show "A --> C"; + proof; + assume A; + show C; + proof (rule mp); + show "B --> C"; by (rule mp); + show B; by (rule mp); + qed; + qed; + qed; +qed; + + end; |