diff options
| -rw-r--r-- | coq/example.v | 2 | ||||
| -rw-r--r-- | isar/Example.thy | 14 | ||||
| -rw-r--r-- | lego/example.l | 13 |
3 files changed, 18 insertions, 11 deletions
diff --git a/coq/example.v b/coq/example.v index 8934a3d8..619072c2 100644 --- a/coq/example.v +++ b/coq/example.v @@ -10,4 +10,4 @@ Induction H. Apply conj. Assumption. Assumption. -Save conj_comms. +Save and_comms. diff --git a/isar/Example.thy b/isar/Example.thy index c213de4d..2b9c72f6 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -1,13 +1,19 @@ +(* + Example proof document for Isabelle/Isar Proof General. + + $Id$ +*) + theory Example = Main:; -lemma and_comms: "A & B --> B & A"; +theorem and_comms: "A & B --> B & A"; proof; assume "A & B"; - show "B & A"; + thus "B & A"; proof; - from prems; show B; ..; - from prems; show A; ..; + assume B A; + thus ?thesis; ..; qed; qed; diff --git a/lego/example.l b/lego/example.l index 4a506990..e5e6d7b8 100644 --- a/lego/example.l +++ b/lego/example.l @@ -6,9 +6,10 @@ Module example Import lib_logic; -Goal and_commutes: {A,B:Prop}(and A B) -> (and B A); -intros; andI; -Refine H; intros; Immed; Refine H; intros; Immed; -Save and_commutes; - - +Goal {A,B:Prop}(and A B) -> (and B A); +intros; +Refine H; +intros; +andI; +Immed; +Save and_comms; |