src/FOL/cladata.ML
changeset 13034 d7bb6e4f5f82
parent 11748 06eb315831ff
child 14156 2072802ab0e3
equal deleted inserted replaced
13033:d6a09050a40d 13034:d7bb6e4f5f82
    10 
    10 
    11 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
    11 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
    12 structure Make_Elim = Make_Elim_Fun(val classical = classical);
    12 structure Make_Elim = Make_Elim_Fun(val classical = classical);
    13 
    13 
    14 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
    14 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
    15   compatibliity with strange things done in many existing proofs *)
    15   compatibility with strange things done in many existing proofs *)
    16 val cla_make_elim = Make_Elim.make_elim;
    16 val cla_make_elim = Make_Elim.make_elim;
    17 
    17 
    18 (*** Applying ClassicalFun to create a classical prover ***)
    18 (*** Applying ClassicalFun to create a classical prover ***)
    19 structure Classical_Data = 
    19 structure Classical_Data = 
    20   struct
    20   struct