author wenzelm Sat, 03 Jul 1999 00:26:00 +0200 changeset 6892 4a905b4a39c8 parent 6891 7bb02d03035d child 6893 6e56603fb339
tuned;
 src/HOL/Isar_examples/BasicLogic.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Group.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/Peirce.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Jul 03 00:23:17 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Jul 03 00:26:00 1999 +0200
@@ -70,10 +70,10 @@

lemma "A & B --> B & A";
proof;
-  assume AB: "A & B";
-  from AB; have A: A; ..;
-  from AB; have B: B; ..;
-  from B A; show "B & A"; ..;
+  assume ab: "A & B";
+  from ab; have a: A; ..;
+  from ab; have b: B; ..;
+  from b a; show "B & A"; ..;
qed;

```
```--- a/src/HOL/Isar_examples/Group.thy	Sat Jul 03 00:23:17 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Sat Jul 03 00:26:00 1999 +0200
@@ -95,19 +95,19 @@
have "... = x * inv x * x";
by (simp add: group_assoc);

-  note calculation = trans[OF calculation facts]
+  note calculation = trans [OF calculation facts]
-- {* general calculational step: compose with transitivity rule *};

have "... = one * x";
by (simp add: group_right_inverse);

-  note calculation = trans[OF calculation facts]
+  note calculation = trans [OF calculation facts]
-- {* general calculational step: compose with transitivity rule *};

have "... = x";
by (simp add: group_left_unit);

-  note calculation = trans[OF calculation facts]
+  note calculation = trans [OF calculation facts]
-- {* final calculational step: compose with transitivity rule ... *};
from calculation
-- {* ... and pick up final result *};```
```--- a/src/HOL/Isar_examples/Peirce.thy	Sat Jul 03 00:23:17 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Sat Jul 03 00:26:00 1999 +0200
@@ -9,35 +9,35 @@

theorem "((A --> B) --> A) --> A";
proof;
-  assume ABA: "(A --> B) --> A";
+  assume aba: "(A --> B) --> A";
show A;
proof (rule classical);
-    assume notA: "~ A";
+    assume not_a: "~ A";

-    have AB: "A --> B";
+    have ab: "A --> B";
proof;
-      assume A: A;
-      from notA A; show B; ..;
+      assume a: A;
+      from not_a a; show B; ..;
qed;

-    from ABA AB; show A; ..;
+    from aba ab; show A; ..;
qed;
qed;

theorem "((A --> B) --> A) --> A";
proof;
-  assume ABA: "(A --> B) --> A";
+  assume aba: "(A --> B) --> A";
show A;
proof (rule classical);
-    presume AB: "A --> B";
-    from ABA AB; show A; ..;
+    presume ab: "A --> B";
+    from aba ab; show A; ..;
next;
-    assume notA: "~ A";
+    assume not_a: "~ A";
show "A --> B";
proof;
-      assume A: A;
-      from notA A; show B; ..;
+      assume a: A;
+      from not_a a; show B; ..;
qed;
qed;
qed;```