src/Pure/axclass.ML
changeset 1201 de2fc8cf9b6a
parent 886 9af08725600b
child 1217 f96a04c6b352
equal deleted inserted replaced
1200:d4551b1a6da7 1201:de2fc8cf9b6a
    64 val get_axioms = mapfilter o get_ax;
    64 val get_axioms = mapfilter o get_ax;
    65 
    65 
    66 val is_def = is_equals o #prop o rep_thm;
    66 val is_def = is_equals o #prop o rep_thm;
    67 
    67 
    68 fun witnesses thy axms thms =
    68 fun witnesses thy axms thms =
    69   get_axioms thy axms @ thms @ filter is_def (map snd (axioms_of thy));
    69   map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy));
    70 
    70 
    71 
    71 
    72 
    72 
    73 (** abstract syntax operations **)
    73 (** abstract syntax operations **)
    74 
    74