structure Thm: less pervasive names;
authorwenzelm
Wed Aug 25 15:12:49 2010 +0200 (2010-08-25 ago)
changeset 3870904414091f3b5
parent 38708 8915e3ce8655
child 38710 c1ff9234c49c
structure Thm: less pervasive names;
src/HOL/Tools/meson.ML
src/Pure/Isar/element.ML
src/Pure/drule.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Wed Aug 25 14:18:09 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Aug 25 15:12:49 2010 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
     1.5  
     1.6  fun flexflex_first_order th =
     1.7 -  case (tpairs_of th) of
     1.8 +  case Thm.tpairs_of th of
     1.9        [] => th
    1.10      | pairs =>
    1.11          let val thy = theory_of_thm th
     2.1 --- a/src/Pure/Isar/element.ML	Wed Aug 25 14:18:09 2010 +0200
     2.2 +++ b/src/Pure/Isar/element.ML	Wed Aug 25 15:12:49 2010 +0200
     2.3 @@ -467,7 +467,7 @@
     2.4  
     2.5  fun transfer_morphism thy =
     2.6    let val thy_ref = Theory.check_thy thy
     2.7 -  in Morphism.thm_morphism (fn th => transfer (Theory.deref thy_ref) th) end;
     2.8 +  in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end;
     2.9  
    2.10  
    2.11  
     3.1 --- a/src/Pure/drule.ML	Wed Aug 25 14:18:09 2010 +0200
     3.2 +++ b/src/Pure/drule.ML	Wed Aug 25 15:12:49 2010 +0200
     3.3 @@ -277,7 +277,7 @@
     3.4  (*Squash a theorem's flexflex constraints provided it can be done uniquely.
     3.5    This step can lose information.*)
     3.6  fun flexflex_unique th =
     3.7 -  if null (tpairs_of th) then th else
     3.8 +  if null (Thm.tpairs_of th) then th else
     3.9      case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
    3.10        [th] => th
    3.11      | []   => raise THM("flexflex_unique: impossible constraints", 0, [th])
     4.1 --- a/src/Pure/thm.ML	Wed Aug 25 14:18:09 2010 +0200
     4.2 +++ b/src/Pure/thm.ML	Wed Aug 25 15:12:49 2010 +0200
     4.3 @@ -59,41 +59,11 @@
     4.4    exception THM of string * int * thm list
     4.5    val theory_of_thm: thm -> theory
     4.6    val prop_of: thm -> term
     4.7 -  val tpairs_of: thm -> (term * term) list
     4.8    val concl_of: thm -> term
     4.9    val prems_of: thm -> term list
    4.10    val nprems_of: thm -> int
    4.11    val cprop_of: thm -> cterm
    4.12    val cprem_of: thm -> int -> cterm
    4.13 -  val transfer: theory -> thm -> thm
    4.14 -  val weaken: cterm -> thm -> thm
    4.15 -  val weaken_sorts: sort list -> cterm -> cterm
    4.16 -  val extra_shyps: thm -> sort list
    4.17 -
    4.18 -  (*meta rules*)
    4.19 -  val assume: cterm -> thm
    4.20 -  val implies_intr: cterm -> thm -> thm
    4.21 -  val implies_elim: thm -> thm -> thm
    4.22 -  val forall_intr: cterm -> thm -> thm
    4.23 -  val forall_elim: cterm -> thm -> thm
    4.24 -  val reflexive: cterm -> thm
    4.25 -  val symmetric: thm -> thm
    4.26 -  val transitive: thm -> thm -> thm
    4.27 -  val beta_conversion: bool -> conv
    4.28 -  val eta_conversion: conv
    4.29 -  val eta_long_conversion: conv
    4.30 -  val abstract_rule: string -> cterm -> thm -> thm
    4.31 -  val combination: thm -> thm -> thm
    4.32 -  val equal_intr: thm -> thm -> thm
    4.33 -  val equal_elim: thm -> thm -> thm
    4.34 -  val flexflex_rule: thm -> thm Seq.seq
    4.35 -  val generalize: string list * string list -> int -> thm -> thm
    4.36 -  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    4.37 -  val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
    4.38 -  val trivial: cterm -> thm
    4.39 -  val dest_state: thm * int -> (term * term) list * term list * term * term
    4.40 -  val lift_rule: cterm -> thm -> thm
    4.41 -  val incr_indexes: int -> thm -> thm
    4.42  end;
    4.43  
    4.44  signature THM =
    4.45 @@ -119,8 +89,13 @@
    4.46    val maxidx_of: thm -> int
    4.47    val maxidx_thm: thm -> int -> int
    4.48    val hyps_of: thm -> term list
    4.49 +  val tpairs_of: thm -> (term * term) list
    4.50    val no_prems: thm -> bool
    4.51    val major_prem_of: thm -> term
    4.52 +  val transfer: theory -> thm -> thm
    4.53 +  val weaken: cterm -> thm -> thm
    4.54 +  val weaken_sorts: sort list -> cterm -> cterm
    4.55 +  val extra_shyps: thm -> sort list
    4.56    val join_proofs: thm list -> unit
    4.57    val proof_body_of: thm -> proof_body
    4.58    val proof_of: thm -> proof
    4.59 @@ -134,21 +109,45 @@
    4.60    val map_tags: (Properties.T -> Properties.T) -> thm -> thm
    4.61    val norm_proof: thm -> thm
    4.62    val adjust_maxidx_thm: int -> thm -> thm
    4.63 -  val varifyT_global: thm -> thm
    4.64 -  val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
    4.65 +  (*meta rules*)
    4.66 +  val assume: cterm -> thm
    4.67 +  val implies_intr: cterm -> thm -> thm
    4.68 +  val implies_elim: thm -> thm -> thm
    4.69 +  val forall_intr: cterm -> thm -> thm
    4.70 +  val forall_elim: cterm -> thm -> thm
    4.71 +  val reflexive: cterm -> thm
    4.72 +  val symmetric: thm -> thm
    4.73 +  val transitive: thm -> thm -> thm
    4.74 +  val beta_conversion: bool -> conv
    4.75 +  val eta_conversion: conv
    4.76 +  val eta_long_conversion: conv
    4.77 +  val abstract_rule: string -> cterm -> thm -> thm
    4.78 +  val combination: thm -> thm -> thm
    4.79 +  val equal_intr: thm -> thm -> thm
    4.80 +  val equal_elim: thm -> thm -> thm
    4.81 +  val flexflex_rule: thm -> thm Seq.seq
    4.82 +  val generalize: string list * string list -> int -> thm -> thm
    4.83 +  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    4.84 +  val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
    4.85 +  val trivial: cterm -> thm
    4.86    val of_class: ctyp * class -> thm
    4.87    val strip_shyps: thm -> thm
    4.88    val unconstrainT: thm -> thm
    4.89 +  val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
    4.90 +  val varifyT_global: thm -> thm
    4.91    val legacy_freezeT: thm -> thm
    4.92 +  val dest_state: thm * int -> (term * term) list * term list * term * term
    4.93 +  val lift_rule: cterm -> thm -> thm
    4.94 +  val incr_indexes: int -> thm -> thm
    4.95    val assumption: int -> thm -> thm Seq.seq
    4.96    val eq_assumption: int -> thm -> thm
    4.97    val rotate_rule: int -> int -> thm -> thm
    4.98    val permute_prems: int -> int -> thm -> thm
    4.99    val rename_params_rule: string list * int -> thm -> thm
   4.100 +  val rename_boundvars: term -> term -> thm -> thm
   4.101    val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   4.102    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   4.103    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   4.104 -  val rename_boundvars: term -> term -> thm -> thm
   4.105    val extern_oracles: theory -> xstring list
   4.106    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   4.107  end;