--- a/src/HOL/IMP/Natural.ML Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Natural.ML Tue Jul 04 10:54:46 2000 +0200
@@ -11,7 +11,7 @@
val evalc_elim_cases =
map evalc.mk_cases
["<SKIP,s> -c-> t",
- "<x:=a,s> -c-> t",
+ "<x:==a,s> -c-> t",
"<c1;c2, s> -c-> t",
"<IF b THEN c1 ELSE c2, s> -c-> t"];
@@ -23,7 +23,7 @@
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
by (etac evalc.induct 1);
by (thin_tac "<?c,s2> -c-> s1" 7);
-(*blast_tac needs Unify.search_bound, trace_bound := 40*)
+(*blast_tac needs Unify.search_bound, trace_bound ::= 40*)
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
qed_spec_mp "com_det";