src/HOLCF/Porder.ML
changeset 11452 f3fbbaeb4fb8
parent 11347 4e41f71179ed
child 12030 46d57d0290a2
     1.1 --- a/src/HOLCF/Porder.ML	Wed Jul 25 13:13:01 2001 +0200
     1.2 +++ b/src/HOLCF/Porder.ML	Wed Jul 25 13:33:08 2001 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
     1.5  
     1.6  Goal "EX x. M <<| x ==> M <<| lub(M)";
     1.7 -by (asm_full_simp_tac (simpset() addsimps [lub, Ex_def]) 1);
     1.8 +by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1);
     1.9  bind_thm ("lubI", exI RS result());
    1.10  
    1.11  Goal "M <<| l ==> lub(M) = l";