src/HOL/HOL.ML
changeset 1980 a22ff848be9b
parent 1918 d898eb4beb96
child 2031 03a843f0f447
     1.1 --- a/src/HOL/HOL.ML	Thu Sep 12 10:32:43 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Thu Sep 12 10:34:01 1996 +0200
     1.3 @@ -347,101 +347,8 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -
     1.8 -(*** Setting up the classical reasoner and simplifier ***)
     1.9 -
    1.10 -
    1.11 -(** Applying HypsubstFun to generate hyp_subst_tac **)
    1.12 -section "Classical Reasoner";
    1.13 -
    1.14 -structure Hypsubst_Data =
    1.15 -  struct
    1.16 -  structure Simplifier = Simplifier
    1.17 -  (*Take apart an equality judgement; otherwise raise Match!*)
    1.18 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
    1.19 -  val eq_reflection = eq_reflection
    1.20 -  val imp_intr = impI
    1.21 -  val rev_mp = rev_mp
    1.22 -  val subst = subst
    1.23 -  val sym = sym
    1.24 -  end;
    1.25 -
    1.26 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.27 -open Hypsubst;
    1.28 -
    1.29 -(*** Applying ClassicalFun to create a classical prover ***)
    1.30 -structure Classical_Data = 
    1.31 -  struct
    1.32 -  val sizef     = size_of_thm
    1.33 -  val mp        = mp
    1.34 -  val not_elim  = notE
    1.35 -  val classical = classical
    1.36 -  val hyp_subst_tacs=[hyp_subst_tac]
    1.37 -  end;
    1.38 -
    1.39 -structure Classical = ClassicalFun(Classical_Data);
    1.40 -open Classical;
    1.41 -
    1.42 -(*Propositional rules*)
    1.43 -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.44 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.45 -
    1.46 -(*Quantifier rules*)
    1.47 -val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    1.48 -                     addSEs [exE,ex1E] addEs [allE];
    1.49 -
    1.50 -exception CS_DATA of claset;
    1.51 -
    1.52 -let fun merge [] = CS_DATA empty_cs
    1.53 -      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
    1.54 -                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
    1.55 -
    1.56 -    fun put (CS_DATA cs) = claset := cs;
    1.57 -
    1.58 -    fun get () = CS_DATA (!claset);
    1.59 -in add_thydata "HOL"
    1.60 -     ("claset", ThyMethods {merge = merge, put = put, get = get})
    1.61 -end;
    1.62 -
    1.63 -claset := HOL_cs;
    1.64 -
    1.65 -section "Simplifier";
    1.66 -
    1.67 -use     "simpdata.ML";
    1.68 -simpset := HOL_ss;
    1.69 -
    1.70 -
    1.71 -(** Install simpsets and datatypes in theory structure **)
    1.72 -exception SS_DATA of simpset;
    1.73 -
    1.74 -let fun merge [] = SS_DATA empty_ss
    1.75 -      | merge ss = let val ss = map (fn SS_DATA x => x) ss;
    1.76 -                   in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
    1.77 -
    1.78 -    fun put (SS_DATA ss) = simpset := ss;
    1.79 -
    1.80 -    fun get () = SS_DATA (!simpset);
    1.81 -in add_thydata "HOL"
    1.82 -     ("simpset", ThyMethods {merge = merge, put = put, get = get})
    1.83 -end;
    1.84 -
    1.85 -type dtype_info = {case_const:term, case_rewrites:thm list,
    1.86 -                   constructors:term list, nchotomy:thm, case_cong:thm};
    1.87 -
    1.88 -exception DT_DATA of (string * dtype_info) list;
    1.89 -val datatypes = ref [] : (string * dtype_info) list ref;
    1.90 -
    1.91 -let fun merge [] = DT_DATA []
    1.92 -      | merge ds =
    1.93 -          let val ds = map (fn DT_DATA x => x) ds;
    1.94 -          in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end;
    1.95 -
    1.96 -    fun put (DT_DATA ds) = datatypes := ds;
    1.97 -
    1.98 -    fun get () = DT_DATA (!datatypes);
    1.99 -in add_thydata "HOL"
   1.100 -     ("datatypes", ThyMethods {merge = merge, put = put, get = get})
   1.101 -end;
   1.102 -
   1.103 -
   1.104 -add_thy_reader_file "thy_data.ML";
   1.105 +(*Thus, assignments to the references claset and simpset are recorded
   1.106 +  with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
   1.107 +use "hologic.ML";
   1.108 +use "cladata.ML";
   1.109 +use "simpdata.ML";