author | paulson |
Thu, 05 Sep 1996 18:42:48 +0200 | |
changeset 1958 | 6f20ecbd87cb |
parent 1957 | 58b60b558e48 |
child 1959 | 58f8379eca73 |
--- a/src/HOL/IMP/Natural.ML Thu Sep 05 18:31:14 1996 +0200 +++ b/src/HOL/IMP/Natural.ML Thu Sep 05 18:42:48 1996 +0200 @@ -18,6 +18,6 @@ (* evaluation of com is deterministic *) goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; by (etac evalc.induct 1); -by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7); +by (thin_tac "<?c,s2> -c-> s1" 7); by (ALLGOALS (deepen_tac evalc_cs 4)); qed_spec_mp "com_det";