Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/smt_normalize.ML
changeset 36899 bcd6fce5bf06
parent 36898 8e55aa1306c5
child 36936 c52d1c130898 
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 12 23:54:02 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 12 23:54:04 2010 +0200
@@ -18,6 +18,7 @@
   type extra_norm = thm list -> Proof.context -> thm list * Proof.context
   val normalize: extra_norm -> thm list -> Proof.context ->
     thm list * Proof.context
+  val atomize_conv: Proof.context -> conv
   val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
 end
isabelle