--- a/src/HOL/Nat.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Nat.ML Mon Jun 22 17:26:46 1998 +0200
@@ -4,17 +4,17 @@
Copyright 1997 TU Muenchen
*)
-goal thy "min 0 n = 0";
+Goal "min 0 n = 0";
by (rtac min_leastL 1);
by (trans_tac 1);
qed "min_0L";
-goal thy "min n 0 = 0";
+Goal "min n 0 = 0";
by (rtac min_leastR 1);
by (trans_tac 1);
qed "min_0R";
-goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
+Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
by (Simp_tac 1);
qed "min_Suc_Suc";