src/FOL/cladata.ML
changeset 9158 084abf3d0eff
parent 8099 6a087be9f6d9
child 9472 b63b21f370ca
equal deleted inserted replaced
9157:998dd2fb5795 9158:084abf3d0eff
     6 Setting up the classical reasoner.
     6 Setting up the classical reasoner.
     7 *)
     7 *)
     8 
     8 
     9 section "Classical Reasoner";
     9 section "Classical Reasoner";
    10 
    10 
       
    11 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
       
    12 structure Make_Elim_Data =
       
    13 struct
       
    14   val classical = classical
       
    15 end;
       
    16 
       
    17 structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
       
    18 
       
    19 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
       
    20   compatibliity with strange things done in many existing proofs *)
       
    21 val cla_make_elim = Make_Elim.make_elim;
    11 
    22 
    12 (*** Applying ClassicalFun to create a classical prover ***)
    23 (*** Applying ClassicalFun to create a classical prover ***)
    13 structure Classical_Data = 
    24 structure Classical_Data = 
    14   struct
    25   struct
    15   val sizef     = size_of_thm
    26   val make_elim = cla_make_elim
    16   val mp        = mp
    27   val mp        = mp
    17   val not_elim  = notE
    28   val not_elim  = notE
    18   val classical = classical
    29   val classical = classical
       
    30   val sizef     = size_of_thm
    19   val hyp_subst_tacs=[hyp_subst_tac]
    31   val hyp_subst_tacs=[hyp_subst_tac]
    20   end;
    32   end;
    21 
    33 
    22 structure Cla = ClassicalFun(Classical_Data);
    34 structure Cla = ClassicalFun(Classical_Data);
    23 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
    35 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;