src/Pure/conv.ML
changeset 32843 c8f5a7c8353f
parent 30136 6a874aedb964
child 36936 c52d1c130898
     1.1 --- a/src/Pure/conv.ML	Thu Oct 01 22:40:29 2009 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu Oct 01 23:27:05 2009 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      Pure/conv.ML
     1.5 -    Author:     Amine Chaieb and Makarius
     1.6 +    Author:     Amine Chaieb, TU Muenchen
     1.7 +    Author:     Makarius
     1.8  
     1.9  Conversions: primitive equality reasoning.
    1.10  *)
    1.11 @@ -22,6 +23,7 @@
    1.12    val every_conv: conv list -> conv
    1.13    val try_conv: conv -> conv
    1.14    val repeat_conv: conv -> conv
    1.15 +  val cache_conv: conv -> conv
    1.16    val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    1.17    val combination_conv: conv -> conv -> conv
    1.18    val comb_conv: conv -> conv
    1.19 @@ -44,7 +46,7 @@
    1.20  structure Conv: CONV =
    1.21  struct
    1.22  
    1.23 -(* conversionals *)
    1.24 +(* basic conversionals *)
    1.25  
    1.26  fun no_conv _ = raise CTERM ("no conversion", []);
    1.27  val all_conv = Thm.reflexive;
    1.28 @@ -72,6 +74,8 @@
    1.29  fun try_conv cv = cv else_conv all_conv;
    1.30  fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    1.31  
    1.32 +fun cache_conv (cv: conv) = Thm.cterm_cache cv;
    1.33 +
    1.34  
    1.35  
    1.36  (** Pure conversions **)
    1.37 @@ -177,5 +181,5 @@
    1.38  
    1.39  end;
    1.40  
    1.41 -structure BasicConv: BASIC_CONV = Conv;
    1.42 -open BasicConv;
    1.43 +structure Basic_Conv: BASIC_CONV = Conv;
    1.44 +open Basic_Conv;