src/Pure/thm.ML
changeset 31945 d5f186aa0bed
parent 31944 c8a35979a5bc
child 31947 7daee3bed3af
     1.1 --- a/src/Pure/thm.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -97,14 +97,6 @@
     1.4    val dest_state: thm * int -> (term * term) list * term list * term * term
     1.5    val lift_rule: cterm -> thm -> thm
     1.6    val incr_indexes: int -> thm -> thm
     1.7 -  val assumption: int -> thm -> thm Seq.seq
     1.8 -  val eq_assumption: int -> thm -> thm
     1.9 -  val rotate_rule: int -> int -> thm -> thm
    1.10 -  val permute_prems: int -> int -> thm -> thm
    1.11 -  val rename_params_rule: string list * int -> thm -> thm
    1.12 -  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
    1.13 -  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    1.14 -  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    1.15  end;
    1.16  
    1.17  signature THM =
    1.18 @@ -117,37 +109,45 @@
    1.19    val dest_fun2: cterm -> cterm
    1.20    val dest_arg1: cterm -> cterm
    1.21    val dest_abs: string option -> cterm -> cterm * cterm
    1.22 -  val adjust_maxidx_cterm: int -> cterm -> cterm
    1.23    val capply: cterm -> cterm -> cterm
    1.24    val cabs: cterm -> cterm -> cterm
    1.25 -  val major_prem_of: thm -> term
    1.26 -  val no_prems: thm -> bool
    1.27 +  val adjust_maxidx_cterm: int -> cterm -> cterm
    1.28 +  val incr_indexes_cterm: int -> cterm -> cterm
    1.29 +  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    1.30 +  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    1.31    val terms_of_tpairs: (term * term) list -> term list
    1.32 +  val full_prop_of: thm -> term
    1.33    val maxidx_of: thm -> int
    1.34    val maxidx_thm: thm -> int -> int
    1.35    val hyps_of: thm -> term list
    1.36 -  val full_prop_of: thm -> term
    1.37 +  val no_prems: thm -> bool
    1.38 +  val major_prem_of: thm -> term
    1.39    val axiom: theory -> string -> thm
    1.40    val axioms_of: theory -> (string * thm) list
    1.41 -  val get_name: thm -> string
    1.42 -  val put_name: string -> thm -> thm
    1.43    val get_tags: thm -> Properties.T
    1.44    val map_tags: (Properties.T -> Properties.T) -> thm -> thm
    1.45    val norm_proof: thm -> thm
    1.46    val adjust_maxidx_thm: int -> thm -> thm
    1.47 -  val rename_boundvars: term -> term -> thm -> thm
    1.48 -  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    1.49 -  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    1.50 -  val incr_indexes_cterm: int -> cterm -> cterm
    1.51    val varifyT: thm -> thm
    1.52    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
    1.53    val freezeT: thm -> thm
    1.54 +  val assumption: int -> thm -> thm Seq.seq
    1.55 +  val eq_assumption: int -> thm -> thm
    1.56 +  val rotate_rule: int -> int -> thm -> thm
    1.57 +  val permute_prems: int -> int -> thm -> thm
    1.58 +  val rename_params_rule: string list * int -> thm -> thm
    1.59 +  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
    1.60 +  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    1.61 +  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    1.62 +  val rename_boundvars: term -> term -> thm -> thm
    1.63    val future: thm future -> cterm -> thm
    1.64    val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
    1.65    val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.66    val proof_body_of: thm -> proof_body
    1.67    val proof_of: thm -> proof
    1.68    val join_proof: thm -> unit
    1.69 +  val get_name: thm -> string
    1.70 +  val put_name: string -> thm -> thm
    1.71    val extern_oracles: theory -> xstring list
    1.72    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    1.73  end;