unified names: foo_conv;
authorwenzelm
Fri May 11 18:46:50 2007 +0200 (2007-05-11)
changeset 2293708cf9aaf3aa1
parent 22936 284b56463da8
child 22938 454f1678bf5f
unified names: foo_conv;
src/Pure/conv.ML
     1.1 --- a/src/Pure/conv.ML	Fri May 11 17:54:36 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Fri May 11 18:46:50 2007 +0200
     1.3 @@ -5,20 +5,20 @@
     1.4  Conversions: primitive equality reasoning.
     1.5  *)
     1.6  
     1.7 -infix 1 thenc;
     1.8 -infix 0 orelsec;
     1.9 +infix 1 then_conv;
    1.10 +infix 0 else_conv;
    1.11  
    1.12  signature CONV =
    1.13  sig
    1.14    type conv = cterm -> thm
    1.15    val no_conv: conv
    1.16    val all_conv: conv
    1.17 -  val thenc: conv * conv -> conv
    1.18 -  val orelsec: conv * conv -> conv
    1.19 +  val then_conv: conv * conv -> conv
    1.20 +  val else_conv: conv * conv -> conv
    1.21    val first_conv: conv list -> conv
    1.22    val every_conv: conv list -> conv
    1.23 -  val tryc: conv -> conv
    1.24 -  val repeatc: conv -> conv
    1.25 +  val try_conv: conv -> conv
    1.26 +  val repeat_conv: conv -> conv
    1.27    val cache_conv: conv -> conv
    1.28    val abs_conv: conv -> conv
    1.29    val combination_conv: conv -> conv -> conv
    1.30 @@ -46,7 +46,7 @@
    1.31  
    1.32  val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    1.33  
    1.34 -fun (cv1 thenc cv2) ct =
    1.35 +fun (cv1 then_conv cv2) ct =
    1.36    let
    1.37      val eq1 = cv1 ct;
    1.38      val eq2 = cv2 (Thm.rhs_of eq1);
    1.39 @@ -56,14 +56,14 @@
    1.40      else Thm.transitive eq1 eq2
    1.41    end;
    1.42  
    1.43 -fun (cv1 orelsec cv2) ct =
    1.44 +fun (cv1 else_conv cv2) ct =
    1.45    (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
    1.46  
    1.47 -fun first_conv cvs = fold_rev (curry op orelsec) cvs no_conv;
    1.48 -fun every_conv cvs = fold_rev (curry op thenc) cvs all_conv;
    1.49 +fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
    1.50 +fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
    1.51  
    1.52 -fun tryc cv = cv orelsec all_conv;
    1.53 -fun repeatc cv ct = tryc (cv thenc repeatc cv) ct;
    1.54 +fun try_conv cv = cv else_conv all_conv;
    1.55 +fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    1.56  
    1.57  fun cache_conv cv =
    1.58    let