src/HOL/Tools/SMT/smt_normalize.ML
changeset 36899 bcd6fce5bf06
parent 36898 8e55aa1306c5
child 36936 c52d1c130898
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 12 23:54:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 12 23:54:04 2010 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    type extra_norm = thm list -> Proof.context -> thm list * Proof.context
     1.5    val normalize: extra_norm -> thm list -> Proof.context ->
     1.6      thm list * Proof.context
     1.7 +  val atomize_conv: Proof.context -> conv
     1.8    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
     1.9  end
    1.10