# HG changeset patch
# User wenzelm
# Date 930954360 -7200
# Node ID 4a905b4a39c8cb58d8e244550f19fef8c4ff7626
# Parent  7bb02d03035d735e2aceb9e7397c368a0589d61a
tuned;

diff -r 7bb02d03035d -r 4a905b4a39c8 src/HOL/Isar_examples/BasicLogic.thy
--- 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;
 
 
diff -r 7bb02d03035d -r 4a905b4a39c8 src/HOL/Isar_examples/Group.thy
--- 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 *};
diff -r 7bb02d03035d -r 4a905b4a39c8 src/HOL/Isar_examples/Peirce.thy
--- 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;