diff -r d8d85a8172b5 -r 36d9f215c982 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML Sat Jul 18 22:58:50 2015 +0200
+++ b/src/HOL/Tools/cnf.ML Sun Jul 19 00:03:10 2015 +0200
@@ -54,41 +54,41 @@
structure CNF : CNF =
struct
-val clause2raw_notE = @{lemma "[| P; ~P |] ==> False" by auto};
-val clause2raw_not_disj = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
-val clause2raw_not_not = @{lemma "P ==> ~~P" by auto};
+val clause2raw_notE = @{lemma "\P; \P\ \ False" by auto};
+val clause2raw_not_disj = @{lemma "\\ P; \ Q\ \ \ (P \ Q)" by auto};
+val clause2raw_not_not = @{lemma "P \ \\ P" by auto};
val iff_refl = @{lemma "(P::bool) = P" by auto};
val iff_trans = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
-val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
-val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
+val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto};
+val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto};
-val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
-val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
+val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto};
+val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' \ NQ) \ (NP \ Q'))" by auto};
val make_nnf_not_false = @{lemma "(~False) = True" by auto};
val make_nnf_not_true = @{lemma "(~True) = False" by auto};
-val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
-val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
-val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
-val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
+val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \ Q)) = (P' \ Q')" by auto};
+val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P \ Q)) = (P' \ Q')" by auto};
+val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P \ Q)) = (P' \ Q')" by auto};
+val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' \ Q') \ (NP \ NQ))" by auto};
val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto};
-val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
-val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
-val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
-val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
-val simp_TF_disj_True_l = @{lemma "P = True ==> (P | Q) = True" by auto};
-val simp_TF_disj_True_r = @{lemma "Q = True ==> (P | Q) = True" by auto};
-val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
-val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
+val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P \ Q) = Q'" by auto};
+val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P \ Q) = P'" by auto};
+val simp_TF_conj_False_l = @{lemma "P = False ==> (P \ Q) = False" by auto};
+val simp_TF_conj_False_r = @{lemma "Q = False ==> (P \ Q) = False" by auto};
+val simp_TF_disj_True_l = @{lemma "P = True ==> (P \ Q) = True" by auto};
+val simp_TF_disj_True_r = @{lemma "Q = True ==> (P \ Q) = True" by auto};
+val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P \ Q) = Q'" by auto};
+val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P \ Q) = P'" by auto};
-val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
-val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
+val make_cnf_disj_conj_l = @{lemma "[| (P \ R) = PR; (Q \ R) = QR |] ==> ((P \ Q) \ R) = (PR \ QR)" by auto};
+val make_cnf_disj_conj_r = @{lemma "[| (P \ Q) = PQ; (P \ R) = PR |] ==> (P \ (Q \ R)) = (PQ \ PR)" by auto};
-val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
-val make_cnfx_disj_ex_r = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
-val make_cnfx_newlit = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
-val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
+val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) \ Q) = (EX x. P x \ Q)" by auto};
+val make_cnfx_disj_ex_r = @{lemma "(P \ (EX (x::bool). Q x)) = (EX x. P \ Q x)" by auto};
+val make_cnfx_newlit = @{lemma "(P \ Q) = (EX x. (P \ x) \ (Q \ ~x))" by auto};
+val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) \ (EX x. P x) = (EX x. Q x)" by auto};
val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto};