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.
removed is_Trueprop (use can dest_Trueprop'' instead);
authorwenzelm
Sat, 04 Nov 2006 19:25:41 +0100
changeset 21174 4d733b76b5fa
parent 21173 663a7b39894c
child 21175 98c0405f5493
removed is_Trueprop (use can dest_Trueprop'' instead);
src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/meson.ML	Sat Nov 04 19:25:40 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Nov 04 19:25:41 2006 +0100
@@ -250,7 +250,7 @@
   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
 fun cnf skoths (th,ths) =
   let fun cnf_aux (th,ths) =
-  	if not (HOLogic.is_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
+  	if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
         else if not (has_conns ["All","Ex","op &"] (prop_of th))  
 	then th::ths (*no work to do, terminate*)
 	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
isabelle