789 val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ())); |
789 val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ())); |
790 val prop_def = get_axiom "prop_def"; |
790 val prop_def = get_axiom "prop_def"; |
791 val term_def = get_axiom "term_def"; |
791 val term_def = get_axiom "term_def"; |
792 in |
792 in |
793 val protect = Thm.capply (certify Logic.protectC); |
793 val protect = Thm.capply (certify Logic.protectC); |
794 val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard |
794 val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard |
795 (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); |
795 (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); |
796 val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard |
796 val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard |
797 (Thm.equal_elim prop_def (Thm.assume (protect A))))); |
797 (Thm.equal_elim prop_def (Thm.assume (protect A))))); |
798 val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); |
798 val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); |
799 |
799 |
800 val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard |
800 val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard |
801 (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); |
801 (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); |
802 end; |
802 end; |
803 |
803 |
804 fun implies_intr_protected asms th = |
804 fun implies_intr_protected asms th = |
805 let val asms' = map protect asms in |
805 let val asms' = map protect asms in |