# HG changeset patch
# User berghofe
# Date 839514353 -7200
# Node ID e349b91cf1975b776987272b66aa6a90ccbd1c34
# Parent  0a4fbd097ce054f186342ed05572e658c8b5423c
Added function for storing default claset in theory.

diff -r 0a4fbd097ce0 -r e349b91cf197 src/ZF/ZF.ML
--- 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";