theory data: finish method;
authorwenzelm
Thu Nov 08 23:59:37 2001 +0100 (2001-11-08)
changeset 12109bd6eb9194a5d
parent 12108 b6f10dcde803
child 12110 f8b4b11cd79d
theory data: finish method;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/arith_data.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Provers/simplifier.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Nov 08 23:57:22 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Nov 08 23:59:37 2001 +0100
     1.3 @@ -94,6 +94,7 @@
     1.4  
     1.5    val empty = Symtab.empty;
     1.6    val copy = I;
     1.7 +  val finish = I;
     1.8    val prep_ext = I;
     1.9    val merge: T * T -> T = Symtab.merge (K true);
    1.10  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Nov 08 23:57:22 2001 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Nov 08 23:59:37 2001 +0100
     2.3 @@ -98,6 +98,7 @@
     2.4  
     2.5    val empty = (Symtab.empty, []);
     2.6    val copy = I;
     2.7 +  val finish = I;
     2.8    val prep_ext = I;
     2.9    fun merge ((tab1, monos1), (tab2, monos2)) =
    2.10      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Nov 08 23:57:22 2001 +0100
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Nov 08 23:59:37 2001 +0100
     3.3 @@ -47,6 +47,7 @@
     3.4  
     3.5    val empty = Symtab.empty;
     3.6    val copy = I;
     3.7 +  val finish = I;
     3.8    val prep_ext = I;
     3.9    val merge: T * T -> T = Symtab.merge (K true);
    3.10  
     4.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Nov 08 23:57:22 2001 +0100
     4.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Nov 08 23:59:37 2001 +0100
     4.3 @@ -111,6 +111,7 @@
     4.4  
     4.5    val empty = (Symtab.empty, mk_hints ([], [], [])): T;
     4.6    val copy = I;
     4.7 +  val finish = I;
     4.8    val prep_ext = I;
     4.9    fun merge
    4.10     ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
     5.1 --- a/src/HOL/Tools/record_package.ML	Thu Nov 08 23:57:22 2001 +0100
     5.2 +++ b/src/HOL/Tools/record_package.ML	Thu Nov 08 23:59:37 2001 +0100
     5.3 @@ -364,6 +364,7 @@
     5.4        {fields = Symtab.empty, simpset = HOL_basic_ss};
     5.5  
     5.6    val copy = I;
     5.7 +  val finish = I;
     5.8    val prep_ext = I;
     5.9    fun merge
    5.10     ({records = recs1,
     6.1 --- a/src/HOL/arith_data.ML	Thu Nov 08 23:57:22 2001 +0100
     6.2 +++ b/src/HOL/arith_data.ML	Thu Nov 08 23:59:37 2001 +0100
     6.3 @@ -213,6 +213,7 @@
     6.4  
     6.5    val empty = {splits = [], inj_consts = [], discrete = []};
     6.6    val copy = I;
     6.7 +  val finish = I;
     6.8    val prep_ext = I;
     6.9    fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
    6.10               {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) =
     7.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Nov 08 23:57:22 2001 +0100
     7.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Nov 08 23:59:37 2001 +0100
     7.3 @@ -100,6 +100,7 @@
     7.4    val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
     7.5                 lessD = [], simpset = Simplifier.empty_ss};
     7.6    val copy = I;
     7.7 +  val finish = I;
     7.8    val prep_ext = I;
     7.9  
    7.10    fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
     8.1 --- a/src/Provers/classical.ML	Thu Nov 08 23:57:22 2001 +0100
     8.2 +++ b/src/Provers/classical.ML	Thu Nov 08 23:59:37 2001 +0100
     8.3 @@ -922,6 +922,7 @@
     8.4  
     8.5    val empty = ref empty_cs;
     8.6    fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
     8.7 +  val finish = I;
     8.8    val prep_ext = copy;
     8.9    fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
    8.10    fun print _ (ref cs) = print_cs cs;
     9.1 --- a/src/Provers/simplifier.ML	Thu Nov 08 23:57:22 2001 +0100
     9.2 +++ b/src/Provers/simplifier.ML	Thu Nov 08 23:59:37 2001 +0100
     9.3 @@ -313,6 +313,7 @@
     9.4  
     9.5    val empty = ref empty_ss;
     9.6    fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
     9.7 +  val finish = I;
     9.8    val prep_ext = copy;
     9.9    fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    9.10    fun print _ (ref ss) = print_ss ss;
    10.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Nov 08 23:57:22 2001 +0100
    10.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Nov 08 23:59:37 2001 +0100
    10.3 @@ -38,6 +38,7 @@
    10.4  
    10.5    val empty = Symtab.empty;
    10.6    val copy = I;
    10.7 +  val finish = I;
    10.8    val prep_ext = I;
    10.9    val merge: T * T -> T = Symtab.merge (K true);
   10.10  
   10.11 @@ -65,6 +66,7 @@
   10.12  
   10.13    val empty = Symtab.empty
   10.14    val copy = I;
   10.15 +  val finish = I;
   10.16    val prep_ext = I
   10.17    val merge: T * T -> T = Symtab.merge (K true)
   10.18  
    11.1 --- a/src/ZF/Tools/typechk.ML	Thu Nov 08 23:57:22 2001 +0100
    11.2 +++ b/src/ZF/Tools/typechk.ML	Thu Nov 08 23:59:37 2001 +0100
    11.3 @@ -95,6 +95,7 @@
    11.4    type T = tcset ref;
    11.5    val empty = ref (TC{rules=[], net=Net.empty});
    11.6    fun copy (ref tc) = ref tc;
    11.7 +  val finish = I;
    11.8    val prep_ext = copy;
    11.9    fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
   11.10    fun print _ (ref tc) = print_tc tc;