author wenzelm Fri, 30 Jul 1999 13:44:29 +0200 changeset 7133 64c9f2364dae parent 7132 5c31d06ead04 child 7134 320b412e5800
renamed 'same' to '-';
 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/KnasterTarski.thy file | annotate | diff | comparison | revisions src/HOL/Isar_examples/NatSum.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Jul 30 13:44:29 1999 +0200
@@ -145,7 +145,7 @@
context again later. *};

theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
-proof same;
+proof -;
assume ab: "A & B";
assume ab_c: "A ==> B ==> C";
show C;```
```--- a/src/HOL/Isar_examples/Group.thy	Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Fri Jul 30 13:44:29 1999 +0200
@@ -32,7 +32,7 @@
*};

theorem group_right_inverse: "x * inv x = (one::'a::group)";
-proof same;
+proof -;
have "x * inv x = one * (x * inv x)";
by (simp only: group_left_unit);
also; have "... = (one * x) * inv x";
@@ -58,7 +58,7 @@
*};

theorem group_right_unit: "x * one = (x::'a::group)";
-proof same;
+proof -;
have "x * one = x * (inv x * x)";
by (simp only: group_left_inverse);
also; have "... = x * inv x * x";
@@ -85,7 +85,7 @@
*};

theorem "x * one = (x::'a::group)";
-proof same;
+proof -;
have "x * one = x * (inv x * x)";
by (simp only: group_left_inverse);
```
```--- a/src/HOL/Isar_examples/KnasterTarski.thy	Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Fri Jul 30 13:44:29 1999 +0200
@@ -25,7 +25,7 @@

assume mono: "mono f";
show "f ??a = ??a";
-  proof same;
+  proof -;
{{;
fix x;
assume mem: "x : ??H";```
```--- a/src/HOL/Isar_examples/NatSum.thy	Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/NatSum.thy	Fri Jul 30 13:44:29 1999 +0200
@@ -34,7 +34,7 @@
*)

theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
-proof same;
+proof -;
apply simp_tac;
apply (induct n);
apply simp_tac;```