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/Meson/meson_clausify.ML
changeset 42351 ad89f5462cdc
parent 42347 53e444ecb525
child 42361 23f352990944 
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:05 2011 +0200
@@ -13,7 +13,6 @@
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
-  val to_definitional_cnf_with_quantifiers : Proof.context -> thm -> thm
   val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
   val ss_only : thm list -> simpset
   val cnf_axiom :
isabelle