src/HOL/HOL.ML
changeset 1725 8b7414384396
parent 1672 2c109cd2fdd0
child 1840 149b2e69633e
     1.1 --- a/src/HOL/HOL.ML	Tue May 07 09:46:25 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Tue May 07 09:53:20 1996 +0200
     1.3 @@ -387,6 +387,20 @@
     1.4  val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
     1.5                       addSEs [exE,ex1E] addEs [allE];
     1.6  
     1.7 +exception CS_DATA of claset;
     1.8 +
     1.9 +let fun merge [] = CS_DATA empty_cs
    1.10 +      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
    1.11 +                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
    1.12 +
    1.13 +    fun put (CS_DATA cs) = claset := cs;
    1.14 +
    1.15 +    fun get () = CS_DATA (!claset);
    1.16 +in add_thydata "HOL"
    1.17 +     ("claset", ThyMethods {merge = merge, put = put, get = get})
    1.18 +end;
    1.19 +
    1.20 +claset := HOL_cs;
    1.21  
    1.22  section "Simplifier";
    1.23  
    1.24 @@ -408,7 +422,6 @@
    1.25       ("simpset", ThyMethods {merge = merge, put = put, get = get})
    1.26  end;
    1.27  
    1.28 -
    1.29  type dtype_info = {case_const:term, case_rewrites:thm list,
    1.30                     constructors:term list, nchotomy:thm, case_cong:thm};
    1.31