src/FOL/ROOT.ML
changeset 2866 0a648ebbf6d4
parent 2469 b50b8c0eec01
child 3511 da4dd8b7ced4
equal deleted inserted replaced
2865:77daca16b2f4 2866:0a648ebbf6d4
    17 
    17 
    18 use "../Provers/splitter.ML";
    18 use "../Provers/splitter.ML";
    19 use "../Provers/ind.ML";
    19 use "../Provers/ind.ML";
    20 use "../Provers/hypsubst.ML";
    20 use "../Provers/hypsubst.ML";
    21 use "../Provers/classical.ML";
    21 use "../Provers/classical.ML";
       
    22 use "../Provers/blast.ML";
    22 
    23 
    23 use_thy "IFOL";
    24 use_thy "IFOL";
    24 
    25 
       
    26 (** Applying HypsubstFun to generate hyp_subst_tac **)
    25 structure Hypsubst_Data =
    27 structure Hypsubst_Data =
    26   struct
    28   struct
    27   structure Simplifier = Simplifier
    29   structure Simplifier = Simplifier
    28     (*Take apart an equality judgement; otherwise raise Match!*)
    30     (*Take apart an equality judgement; otherwise raise Match!*)
    29   fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u)
    31   fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u)