Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove needless export
authorblanchet
Thu, 14 Apr 2011 11:24:05 +0200
changeset 42351 ad89f5462cdc
parent 42350 128dc0fa87fc
child 42352 69221145175d
remove needless export
src/HOL/Tools/Meson/meson_clausify.ML file | annotate | diff | comparison | revisions 
--- 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