src/FOL/cladata.ML
changeset 10429 8820f787e61e
parent 10383 a092ae7bb2a6
child 10906 de95ba2760fe
equal deleted inserted replaced
10428:8f15fbce549f 10429:8820f787e61e
    22   val mp        = mp
    22   val mp        = mp
    23   val not_elim  = notE
    23   val not_elim  = notE
    24   val classical = classical
    24   val classical = classical
    25   val sizef     = size_of_thm
    25   val sizef     = size_of_thm
    26   val hyp_subst_tacs=[hyp_subst_tac]
    26   val hyp_subst_tacs=[hyp_subst_tac]
    27   val atomize	= thms "atomize"
    27   val atomize	= thms "atomize'"
    28   end;
    28   end;
    29 
    29 
    30 structure Cla = ClassicalFun(Classical_Data);
    30 structure Cla = ClassicalFun(Classical_Data);
    31 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
    31 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
    32 
    32