equal
deleted
inserted
replaced
654 @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\ |
654 @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\ |
655 @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\ |
655 @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\ |
656 @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ |
656 @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ |
657 @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\ |
657 @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\ |
658 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ |
658 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ |
659 @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\ |
659 @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
|
660 -> thm -> thm"} \\ |
660 @{index_ML Thm.add_axiom: "Proof.context -> |
661 @{index_ML Thm.add_axiom: "Proof.context -> |
661 binding * term -> theory -> (string * thm) * theory"} \\ |
662 binding * term -> theory -> (string * thm) * theory"} \\ |
662 @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> |
663 @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> |
663 (string * ('a -> thm)) * theory"} \\ |
664 (string * ('a -> thm)) * theory"} \\ |
664 @{index_ML Thm.add_def: "Proof.context -> bool -> bool -> |
665 @{index_ML Thm.add_def: "Proof.context -> bool -> bool -> |