| changeset 4089 | 96fba19bcbe2 |
| parent 1973 | 8c94c9a5be10 |
| child 4241 | 3f3f87c6fe3b |
--- a/src/HOL/IMP/Natural.ML Mon Nov 03 12:12:10 1997 +0100 +++ b/src/HOL/IMP/Natural.ML Mon Nov 03 12:13:18 1997 +0100 @@ -20,5 +20,5 @@ goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; by (etac evalc.induct 1); by (thin_tac "<?c,s2> -c-> s1" 7); -by (ALLGOALS (deepen_tac (!claset addEs [evalc_WHILE_case]) 4)); +by (ALLGOALS (deepen_tac (claset() addEs [evalc_WHILE_case]) 4)); qed_spec_mp "com_det";