src/Pure/drule.ML
changeset 8550 b44c185f8018
parent 8496 7e4a466b18d5
child 8605 625fbbe5c6b4
equal deleted inserted replaced
8549:851d39c10d9f 8550:b44c185f8018
    74   val revcut_rl         : thm
    74   val revcut_rl         : thm
    75   val thin_rl           : thm
    75   val thin_rl           : thm
    76   val triv_forall_equality: thm
    76   val triv_forall_equality: thm
    77   val swap_prems_rl     : thm
    77   val swap_prems_rl     : thm
    78   val equal_intr_rule   : thm
    78   val equal_intr_rule   : thm
       
    79   val inst              : string -> string -> thm -> thm
    79   val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
    80   val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
    80   val incr_indexes      : int -> thm -> thm
    81   val incr_indexes      : int -> thm -> thm
    81   val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    82   val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
    82 end;
    83 end;
    83 
    84 
   627 
   628 
   628 
   629 
   629 
   630 
   630 (** variations on instantiate **)
   631 (** variations on instantiate **)
   631 
   632 
       
   633 (*shorthand for instantiating just one variable in the current theory*)
       
   634 fun inst x t = read_instantiate_sg (sign_of (the_context())) [(x,t)];
       
   635 
       
   636 
   632 (* collect vars *)
   637 (* collect vars *)
   633 
   638 
   634 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
   639 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
   635 val add_tvars = foldl_types add_tvarsT;
   640 val add_tvars = foldl_types add_tvarsT;
   636 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
   641 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);