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/cnf_funcs.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39035 094848cf7ef3 
--- a/src/HOL/Tools/cnf_funcs.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/cnf_funcs.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -98,7 +98,7 @@
   | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
-  | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
+  | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   | is_atom _                                                              = true;
 
@@ -205,7 +205,7 @@
 	in
 		make_nnf_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -239,7 +239,7 @@
 	in
 		make_nnf_not_imp OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
isabelle