equal
deleted
inserted
replaced
595 |
595 |
596 fun class_const c = |
596 fun class_const c = |
597 (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); |
597 (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); |
598 |
598 |
599 fun class_const_dep c = |
599 fun class_const_dep c = |
600 ((Defs.Constant, Logic.const_of_class c), [Term.aT []]); |
600 ((Defs.Const, Logic.const_of_class c), [Term.aT []]); |
601 |
601 |
602 in |
602 in |
603 |
603 |
604 val classrel_axiomatization = |
604 val classrel_axiomatization = |
605 add_axioms (map o cert_classrel) (map Logic.mk_classrel) |
605 add_axioms (map o cert_classrel) (map Logic.mk_classrel) |