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