src/Pure/drule.ML
changeset 5311 f3f71669878e
parent 5079 2a8ed71f791f
child 5688 7f582495967c
equal deleted inserted replaced
5310:3e14d6d66dab 5311:f3f71669878e
    71   val revcut_rl		: thm
    71   val revcut_rl		: thm
    72   val thin_rl		: thm
    72   val thin_rl		: thm
    73   val triv_forall_equality: thm
    73   val triv_forall_equality: thm
    74   val swap_prems_rl     : thm
    74   val swap_prems_rl     : thm
    75   val equal_intr_rule   : thm
    75   val equal_intr_rule   : thm
    76   val triv_goal: thm
    76   val triv_goal		: thm
    77   val rev_triv_goal: thm
    77   val rev_triv_goal	: thm
    78   val instantiate': ctyp option list -> cterm option list -> thm -> thm
    78   val mk_triv_goal      : cterm -> thm
       
    79   val instantiate'	: ctyp option list -> cterm option list -> thm -> thm
    79 end;
    80 end;
    80 
    81 
    81 structure Drule : DRULE =
    82 structure Drule : DRULE =
    82 struct
    83 struct
    83 
    84 
   628       if forall is_none cts then thm'
   629       if forall is_none cts then thm'
   629       else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm'
   630       else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm'
   630     end;
   631     end;
   631 
   632 
   632 
   633 
       
   634 (*Make an initial proof state, "PROP A ==> (PROP A)" *)
       
   635 fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
       
   636 
   633 end;
   637 end;
   634 
   638 
   635 open Drule;
   639 open Drule;