legacy Drule.standard is no longer pervasive;
authorwenzelm
Sat Oct 17 00:53:18 2009 +0200 (2009-10-17)
changeset 329583228627994d9
parent 32957 675c0c7e6a37
child 32959 23a8c5ac35f8
legacy Drule.standard is no longer pervasive;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Oct 17 00:52:37 2009 +0200
     1.2 +++ b/src/Pure/drule.ML	Sat Oct 17 00:53:18 2009 +0200
     1.3 @@ -29,8 +29,6 @@
     1.4    val zero_var_indexes_list: thm list -> thm list
     1.5    val zero_var_indexes: thm -> thm
     1.6    val implies_intr_hyps: thm -> thm
     1.7 -  val standard: thm -> thm
     1.8 -  val standard': thm -> thm
     1.9    val rotate_prems: int -> thm -> thm
    1.10    val rearrange_prems: int list -> thm -> thm
    1.11    val RSN: thm * (int * thm) -> thm
    1.12 @@ -77,6 +75,8 @@
    1.13    val beta_conv: cterm -> cterm -> cterm
    1.14    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    1.15    val flexflex_unique: thm -> thm
    1.16 +  val standard: thm -> thm
    1.17 +  val standard': thm -> thm
    1.18    val get_def: theory -> xstring -> thm
    1.19    val store_thm: bstring -> thm -> thm
    1.20    val store_standard_thm: bstring -> thm -> thm