src/Pure/drule.ML
changeset 60323 9b3b812e6957
parent 60320 e7c0ca878120
child 60367 e201bd8973db
equal deleted inserted replaced
60322:05fabeb0130a 60323:9b3b812e6957
    11   val mk_implies: cterm * cterm -> cterm
    11   val mk_implies: cterm * cterm -> cterm
    12   val list_implies: cterm list * cterm -> cterm
    12   val list_implies: cterm list * cterm -> cterm
    13   val strip_imp_prems: cterm -> cterm list
    13   val strip_imp_prems: cterm -> cterm list
    14   val strip_imp_concl: cterm -> cterm
    14   val strip_imp_concl: cterm -> cterm
    15   val cprems_of: thm -> cterm list
    15   val cprems_of: thm -> cterm list
    16   val cterm_fun: (term -> term) -> (cterm -> cterm)
       
    17   val forall_intr_list: cterm list -> thm -> thm
    16   val forall_intr_list: cterm list -> thm -> thm
    18   val forall_intr_vars: thm -> thm
    17   val forall_intr_vars: thm -> thm
    19   val forall_elim_list: cterm list -> thm -> thm
    18   val forall_elim_list: cterm list -> thm -> thm
    20   val gen_all: int -> thm -> thm
    19   val gen_all: int -> thm -> thm
    21   val lift_all: cterm -> thm -> thm
    20   val lift_all: cterm -> thm -> thm
   128   | _ => ct);
   127   | _ => ct);
   129 
   128 
   130 (*The premises of a theorem, as a cterm list*)
   129 (*The premises of a theorem, as a cterm list*)
   131 val cprems_of = strip_imp_prems o Thm.cprop_of;
   130 val cprems_of = strip_imp_prems o Thm.cprop_of;
   132 
   131 
   133 fun cterm_fun f ct = Thm.global_cterm_of (Thm.theory_of_cterm ct) (f (Thm.term_of ct));
       
   134 
       
   135 fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
   132 fun certify t = Thm.global_cterm_of (Context.the_theory (Context.the_thread_data ())) t;
   136 
   133 
   137 val implies = certify Logic.implies;
   134 val implies = certify Logic.implies;
   138 fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
   135 fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
   139 
   136