| changeset 5183 | 89f162de39cf |
| parent 5117 | 7b5efef2ca74 |
| child 5223 | 4cb05273f764 |
--- a/src/HOL/IMP/Denotation.ML Fri Jul 24 13:02:01 1998 +0200 +++ b/src/HOL/IMP/Denotation.ML Fri Jul 24 13:03:20 1998 +0200 @@ -42,7 +42,7 @@ (* Denotational Semantics implies Operational Semantics *) Goal "!s t. (s,t):C(c) --> <c,s> -c-> t"; -by (com.induct_tac "c" 1); +by (induct_tac "c" 1); by (ALLGOALS Full_simp_tac); by (ALLGOALS (TRY o Fast_tac));