--- a/src/ZF/ZF.ML Thu Aug 08 11:45:04 1996 +0200
+++ b/src/ZF/ZF.ML Thu Aug 08 16:25:53 1996 +0200
@@ -8,6 +8,20 @@
open ZF;
+exception CS_DATA of claset;
+
+let fun merge [] = CS_DATA empty_cs
+ | merge cs = let val cs = map (fn CS_DATA x => x) cs;
+ in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
+
+ fun put (CS_DATA cs) = claset := cs;
+
+ fun get () = CS_DATA (!claset);
+in add_thydata "ZF"
+ ("claset", ThyMethods {merge = merge, put = put, get = get})
+end;
+
+claset:=empty_cs;
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *)
goal ZF.thy "!!a b A. [| b:A; a=b |] ==> a:A";
@@ -446,3 +460,6 @@
qed_goal "Union_in_Pow" ZF.thy
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"
(fn _ => [fast_tac lemmas_cs 1]);
+
+
+add_thy_reader_file "thy_data.ML";