moved aconvc to more_thm.ML;
authorwenzelm
Thu May 31 18:31:36 2007 +0200 (2007-05-31)
changeset 2316937091da05d8e
parent 23168 fcdd4346fa6b
child 23170 94e9413bd7fc
moved aconvc to more_thm.ML;
src/Pure/conv.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/conv.ML	Thu May 31 18:16:59 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu May 31 18:31:36 2007 +0200
     1.3 @@ -7,11 +7,10 @@
     1.4  
     1.5  infix 1 then_conv;
     1.6  infix 0 else_conv;
     1.7 -infix aconvc;
     1.8 +
     1.9  signature CONV =
    1.10  sig
    1.11    type conv = cterm -> thm
    1.12 -  val aconvc : cterm * cterm -> bool
    1.13    val no_conv: conv
    1.14    val all_conv: conv
    1.15    val then_conv: conv * conv -> conv
    1.16 @@ -43,8 +42,6 @@
    1.17  
    1.18  type conv = cterm -> thm;
    1.19  
    1.20 -fun s aconvc t = term_of s aconv term_of t;
    1.21 -
    1.22  fun no_conv _ = raise CTERM ("no conversion", []);
    1.23  val all_conv = Thm.reflexive;
    1.24  
    1.25 @@ -106,6 +103,7 @@
    1.26  
    1.27  fun binop_conv cv = combination_conv (arg_conv cv) cv;
    1.28  
    1.29 +
    1.30  (* logic *)
    1.31  
    1.32  (*rewrite B in !!x1 ... xn. B*)
     2.1 --- a/src/Pure/more_thm.ML	Thu May 31 18:16:59 2007 +0200
     2.2 +++ b/src/Pure/more_thm.ML	Thu May 31 18:31:36 2007 +0200
     2.3 @@ -5,6 +5,8 @@
     2.4  Further operations on type ctyp/cterm/thm, outside the inference kernel.
     2.5  *)
     2.6  
     2.7 +infix aconvc;
     2.8 +
     2.9  signature THM =
    2.10  sig
    2.11    include THM
    2.12 @@ -17,6 +19,7 @@
    2.13    val lhs_of: thm -> cterm
    2.14    val rhs_of: thm -> cterm
    2.15    val thm_ord: thm * thm -> order
    2.16 +  val aconvc : cterm * cterm -> bool
    2.17    val eq_thm: thm * thm -> bool
    2.18    val eq_thms: thm list * thm list -> bool
    2.19    val eq_thm_thy: thm * thm -> bool
    2.20 @@ -99,6 +102,8 @@
    2.21  
    2.22  (* equality *)
    2.23  
    2.24 +val op aconvc = op aconv o pairself Thm.term_of;
    2.25 +
    2.26  fun eq_thm ths =
    2.27    Context.joinable (pairself Thm.theory_of_thm ths) andalso
    2.28    thm_ord ths = EQUAL;