| changeset 1465 | 5d7a7e439cec |
| parent 1440 | de6f18da81bb |
| child 1899 | 0075a8d26a80 |
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML Tue Jan 30 15:24:36 1996 +0100 @@ -58,7 +58,7 @@ (*"'a dual" is even an isotype*) goal thy "Rep_dual (Abs_dual y) = y"; br Abs_dual_inverse 1; - by (rewrite_goals_tac [dual_def]); + by (rewtac dual_def); by (fast_tac set_cs 1); qed "Abs_dual_inverse'";