removed reference to Ex_def
authorpaulson
Wed, 25 Jul 2001 13:33:08 +0200
changeset 11452 f3fbbaeb4fb8
parent 11451 8abfb4f7bd02
child 11453 1b15f655da2c
removed reference to Ex_def
src/HOLCF/Porder.ML
--- 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";