author | paulson |
Wed, 25 Jul 2001 13:33:08 +0200 | |
changeset 11452 | f3fbbaeb4fb8 |
parent 11451 | 8abfb4f7bd02 |
child 11453 | 1b15f655da2c |
--- a/src/HOLCF/Porder.ML Wed Jul 25 13:13:01 2001 +0200 +++ b/src/HOLCF/Porder.ML Wed Jul 25 13:33:08 2001 +0200 @@ -50,7 +50,7 @@ bind_thm("lub",lub_def RS meta_eq_to_obj_eq); Goal "EX x. M <<| x ==> M <<| lub(M)"; -by (asm_full_simp_tac (simpset() addsimps [lub, Ex_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1); bind_thm ("lubI", exI RS result()); Goal "M <<| l ==> lub(M) = l";