equal
deleted
inserted
replaced
415 |
415 |
416 val prove_arity = prove mk_arity (fn thy => fn (t, Ss, c) => |
416 val prove_arity = prove mk_arity (fn thy => fn (t, Ss, c) => |
417 Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c])); |
417 Pretty.string_of_arity (Sign.pp thy) (t, Ss, [c])); |
418 |
418 |
419 fun witnesses thy names thms = |
419 fun witnesses thy names thms = |
420 PureThy.get_thmss thy (map (rpair NONE) names) @ |
420 PureThy.get_thmss thy (map Name names) @ |
421 thms @ |
421 thms @ |
422 List.filter is_def (map snd (axioms_of thy)); |
422 List.filter is_def (map snd (axioms_of thy)); |
423 |
423 |
424 in |
424 in |
425 |
425 |