# HG changeset patch
# User wenzelm
# Date 933335069 -7200
# Node ID 64c9f2364dae267a32a7bc33c3817d049de5afe6
# Parent  5c31d06ead04e1b75506988e58f9927d8b949b6a
renamed 'same' to '-';

diff -r 5c31d06ead04 -r 64c9f2364dae src/HOL/Isar_examples/BasicLogic.thy
--- 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;
diff -r 5c31d06ead04 -r 64c9f2364dae src/HOL/Isar_examples/Group.thy
--- 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);
 
diff -r 5c31d06ead04 -r 64c9f2364dae src/HOL/Isar_examples/KnasterTarski.thy
--- 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";
diff -r 5c31d06ead04 -r 64c9f2364dae src/HOL/Isar_examples/NatSum.thy
--- 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;