add missing strictify rule to proof script
authorhuffman
Mon, 01 Mar 2010 11:15:18 -0800
changeset 35488 eb0fd03d34f9
parent 35487 d1630f317ed0
child 35489 dd02201d95b6
add missing strictify rule to proof script
src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 10:00:14 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 11:15:18 2010 -0800
@@ -507,7 +507,7 @@
           val concl = mk_trp (mk_eq (lhs, rhs));
           val goal = Logic.list_implies (assms, concl);
           val defs = case_beta :: con_betas;
-          val rules1 = @{thms sscase2 sscase3 ssplit2 fup2 ID1};
+          val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
           val rules2 = @{thms con_defined_iff_rules};
           val rules3 = @{thms cfcomp2 one_when2};
           val rules = abs_inverse :: rules1 @ rules2 @ rules3;