src/HOL/cladata.ML
changeset 10429 8820f787e61e
parent 10383 a092ae7bb2a6
child 10906 de95ba2760fe
equal deleted inserted replaced
10428:8f15fbce549f 10429:8820f787e61e
    45   val mp        = mp
    45   val mp        = mp
    46   val not_elim  = notE
    46   val not_elim  = notE
    47   val classical = classical
    47   val classical = classical
    48   val sizef     = size_of_thm
    48   val sizef     = size_of_thm
    49   val hyp_subst_tacs=[hyp_subst_tac]
    49   val hyp_subst_tacs=[hyp_subst_tac]
    50   val atomize	= thms "atomize"
    50   val atomize	= thms "atomize'"
    51   end;
    51   end;
    52 
    52 
    53 structure Classical = ClassicalFun(Classical_Data);
    53 structure Classical = ClassicalFun(Classical_Data);
    54 
    54 
    55 structure BasicClassical: BASIC_CLASSICAL = Classical; 
    55 structure BasicClassical: BASIC_CLASSICAL = Classical;