add take_strict_thms field to take_info type
authorhuffman
Thu Oct 14 10:16:46 2010 -0700 (2010-10-14)
changeset 400152fda96749081
parent 40014 7469b323e260
child 40016 2eff1cbc1ccb
add take_strict_thms field to take_info type
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_take_proofs.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Oct 14 09:44:40 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Oct 14 10:16:46 2010 -0700
     1.3 @@ -639,9 +639,8 @@
     1.4      val (take_info, thy) =
     1.5          Domain_Take_Proofs.define_take_functions
     1.6            (dbinds ~~ iso_infos) thy;
     1.7 -    val { take_consts, take_defs, chain_take_thms, take_0_thms,
     1.8 -          take_Suc_thms, deflation_take_thms,
     1.9 -          finite_consts, finite_defs } = take_info;
    1.10 +    val { take_consts, chain_take_thms, take_0_thms, take_Suc_thms, ...} =
    1.11 +        take_info;
    1.12  
    1.13      (* least-upper-bound lemma for take functions *)
    1.14      val lub_take_lemma =
     2.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Oct 14 09:44:40 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Oct 14 10:16:46 2010 -0700
     2.3 @@ -24,6 +24,7 @@
     2.4        take_0_thms : thm list,
     2.5        take_Suc_thms : thm list,
     2.6        deflation_take_thms : thm list,
     2.7 +      take_strict_thms : thm list,
     2.8        finite_consts : term list,
     2.9        finite_defs : thm list
    2.10      }
    2.11 @@ -35,6 +36,7 @@
    2.12        take_0_thms         : thm list,
    2.13        take_Suc_thms       : thm list,
    2.14        deflation_take_thms : thm list,
    2.15 +      take_strict_thms    : thm list,
    2.16        finite_consts       : term list,
    2.17        finite_defs         : thm list,
    2.18        lub_take_thms       : thm list,
    2.19 @@ -80,6 +82,7 @@
    2.20      take_0_thms : thm list,
    2.21      take_Suc_thms : thm list,
    2.22      deflation_take_thms : thm list,
    2.23 +    take_strict_thms : thm list,
    2.24      finite_consts : term list,
    2.25      finite_defs : thm list
    2.26    };
    2.27 @@ -92,6 +95,7 @@
    2.28      take_0_thms         : thm list,
    2.29      take_Suc_thms       : thm list,
    2.30      deflation_take_thms : thm list,
    2.31 +    take_strict_thms    : thm list,
    2.32      finite_consts       : term list,
    2.33      finite_defs         : thm list,
    2.34      lub_take_thms       : thm list,
    2.35 @@ -429,6 +433,7 @@
    2.36          take_0_thms = take_0_thms,
    2.37          take_Suc_thms = take_Suc_thms,
    2.38          deflation_take_thms = deflation_take_thms,
    2.39 +        take_strict_thms = take_strict_thms,
    2.40          finite_consts = finite_consts,
    2.41          finite_defs = finite_defs
    2.42        };
    2.43 @@ -593,6 +598,7 @@
    2.44          take_0_thms         = #take_0_thms take_info,
    2.45          take_Suc_thms       = #take_Suc_thms take_info,
    2.46          deflation_take_thms = #deflation_take_thms take_info,
    2.47 +        take_strict_thms    = #take_strict_thms take_info,
    2.48          finite_consts       = #finite_consts take_info,
    2.49          finite_defs         = #finite_defs take_info,
    2.50          lub_take_thms       = lub_take_thms,