1.1 --- a/src/HOL/HOL.ML Fri Jan 26 20:25:39 1996 +0100
1.2 +++ b/src/HOL/HOL.ML Mon Jan 29 13:48:37 1996 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: HOL/hol.ML
1.5 +(* Title: HOL/HOL.ML
1.6 ID: $Id$
1.7 Author: Tobias Nipkow
1.8 Copyright 1991 University of Cambridge
1.9 @@ -312,3 +312,35 @@
1.10
1.11 use "simpdata.ML";
1.12 simpset := HOL_ss;
1.13 +
1.14 +
1.15 +(** Install simpsets and datatypes in theory structure **)
1.16 +exception SS_DATA of simpset;
1.17 +
1.18 +let fun merge [] = SS_DATA empty_ss
1.19 + | merge ss = let val ss = map (fn SS_DATA x => x) ss;
1.20 + in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
1.21 +
1.22 + fun put (SS_DATA ss) = simpset := ss;
1.23 +
1.24 + fun get () = SS_DATA (!simpset);
1.25 +in add_thydata HOL.thy
1.26 + ("simpset", ThyMethods {merge = merge, put = put, get = get})
1.27 +end;
1.28 +
1.29 +exception DT_DATA of string list;
1.30 +val datatypes = ref [] : string list ref;
1.31 +
1.32 +let fun merge [] = DT_DATA []
1.33 + | merge ds = let val ds = map (fn DT_DATA x => x) ds;
1.34 + in DT_DATA (foldl (op union) (hd ds, tl ds)) end;
1.35 +
1.36 + fun put (DT_DATA ds) = datatypes := ds;
1.37 +
1.38 + fun get () = DT_DATA (!datatypes);
1.39 +in add_thydata HOL.thy
1.40 + ("datatypes", ThyMethods {merge = merge, put = put, get = get})
1.41 +end;
1.42 +
1.43 +
1.44 +add_thy_reader_file "thy_data.ML";