# HG changeset patch
# User wenzelm
# Date 1445279369 -7200
# Node ID f8cb97e0fd0b47c39d507e2a1efa44ab1136eebe
# Parent  3590367b0ce97d26a8be407048075886f8ff1eeb
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;

diff -r 3590367b0ce9 -r f8cb97e0fd0b src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Oct 19 17:45:36 2015 +0200
+++ b/src/FOL/FOL.thy	Mon Oct 19 20:29:29 2015 +0200
@@ -17,7 +17,7 @@
 subsection \<open>The classical axiom\<close>
 
 axiomatization where
-  classical: "(~P ==> P) ==> P"
+  classical: "(\<not> P \<Longrightarrow> P) \<Longrightarrow> P"
 
 
 subsection \<open>Lemmas and proof tools\<close>
@@ -25,40 +25,41 @@
 lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
   by (erule FalseE [THEN classical])
 
-(*** Classical introduction rules for | and EX ***)
 
-lemma disjCI: "(~Q ==> P) ==> P|Q"
+subsubsection \<open>Classical introduction rules for @{text "\<or>"} and @{text "\<exists>"}\<close>
+
+lemma disjCI: "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"
   apply (rule classical)
   apply (assumption | erule meta_mp | rule disjI1 notI)+
   apply (erule notE disjI2)+
   done
 
-(*introduction rule involving only EX*)
+text \<open>Introduction rule involving only @{text "\<exists>"}\<close>
 lemma ex_classical:
-  assumes r: "~(EX x. P(x)) ==> P(a)"
-  shows "EX x. P(x)"
+  assumes r: "\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)"
+  shows "\<exists>x. P(x)"
   apply (rule classical)
   apply (rule exI, erule r)
   done
 
-(*version of above, simplifying ~EX to ALL~ *)
+text \<open>Version of above, simplifying @{text "\<not>\<exists>"} to @{text "\<forall>\<not>"}.\<close>
 lemma exCI:
-  assumes r: "ALL x. ~P(x) ==> P(a)"
-  shows "EX x. P(x)"
+  assumes r: "\<forall>x. \<not> P(x) \<Longrightarrow> P(a)"
+  shows "\<exists>x. P(x)"
   apply (rule ex_classical)
   apply (rule notI [THEN allI, THEN r])
   apply (erule notE)
   apply (erule exI)
   done
 
-lemma excluded_middle: "~P | P"
+lemma excluded_middle: "\<not> P \<or> P"
   apply (rule disjCI)
   apply assumption
   done
 
 lemma case_split [case_names True False]:
-  assumes r1: "P ==> Q"
-    and r2: "~P ==> Q"
+  assumes r1: "P \<Longrightarrow> Q"
+    and r2: "\<not> P \<Longrightarrow> Q"
   shows Q
   apply (rule excluded_middle [THEN disjE])
   apply (erule r2)
@@ -67,7 +68,7 @@
 
 ML \<open>
   fun case_tac ctxt a fixes =
-    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}
+    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
 \<close>
 
 method_setup case_tac = \<open>
@@ -76,14 +77,13 @@
 \<close> "case_tac emulation (dynamic instantiation!)"
 
 
-(*** Special elimination rules *)
-
+subsection \<open>Special elimination rules\<close>
 
-(*Classical implies (-->) elimination. *)
+text \<open>Classical implies (@{text "\<longrightarrow>"}) elimination.\<close>
 lemma impCE:
-  assumes major: "P-->Q"
-    and r1: "~P ==> R"
-    and r2: "Q ==> R"
+  assumes major: "P \<longrightarrow> Q"
+    and r1: "\<not> P \<Longrightarrow> R"
+    and r2: "Q \<Longrightarrow> R"
   shows R
   apply (rule excluded_middle [THEN disjE])
    apply (erule r1)
@@ -91,13 +91,15 @@
   apply (erule major [THEN mp])
   done
 
-(*This version of --> elimination works on Q before P.  It works best for
-  those cases in which P holds "almost everywhere".  Can't install as
-  default: would break old proofs.*)
+text \<open>
+  This version of @{text "\<longrightarrow>"} elimination works on @{text Q} before @{text
+  P}. It works best for those cases in which P holds ``almost everywhere''.
+  Can't install as default: would break old proofs.
+\<close>
 lemma impCE':
-  assumes major: "P-->Q"
-    and r1: "Q ==> R"
-    and r2: "~P ==> R"
+  assumes major: "P \<longrightarrow> Q"
+    and r1: "Q \<Longrightarrow> R"
+    and r2: "\<not> P \<Longrightarrow> R"
   shows R
   apply (rule excluded_middle [THEN disjE])
    apply (erule r2)
@@ -105,27 +107,30 @@
   apply (erule major [THEN mp])
   done
 
-(*Double negation law*)
-lemma notnotD: "~~P ==> P"
+text \<open>Double negation law.\<close>
+lemma notnotD: "\<not> \<not> P \<Longrightarrow> P"
   apply (rule classical)
   apply (erule notE)
   apply assumption
   done
 
-lemma contrapos2:  "[| Q; ~ P ==> ~ Q |] ==> P"
+lemma contrapos2:  "\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P"
   apply (rule classical)
   apply (drule (1) meta_mp)
   apply (erule (1) notE)
   done
 
-(*** Tactics for implication and contradiction ***)
+
+subsubsection \<open>Tactics for implication and contradiction\<close>
 
-(*Classical <-> elimination.  Proof substitutes P=Q in
-    ~P ==> ~Q    and    P ==> Q  *)
+text \<open>
+  Classical @{text "\<longleftrightarrow>"} elimination. Proof substitutes @{text "P = Q"} in
+  @{text "\<not> P \<Longrightarrow> \<not> Q"} and @{text "P \<Longrightarrow> Q"}.
+\<close>
 lemma iffCE:
-  assumes major: "P<->Q"
-    and r1: "[| P; Q |] ==> R"
-    and r2: "[| ~P; ~Q |] ==> R"
+  assumes major: "P \<longleftrightarrow> Q"
+    and r1: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
+    and r2: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
   shows R
   apply (rule major [unfolded iff_def, THEN conjE])
   apply (elim impCE)
@@ -137,8 +142,8 @@
 
 (*Better for fast_tac: needs no quantifier duplication!*)
 lemma alt_ex1E:
-  assumes major: "EX! x. P(x)"
-    and r: "!!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R"
+  assumes major: "\<exists>! x. P(x)"
+    and r: "\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
   shows R
   using major
 proof (rule ex1E)
@@ -147,19 +152,22 @@
   assume "P(x)"
   then show R
   proof (rule r)
-    { fix y y'
+    {
+      fix y y'
       assume "P(y)" and "P(y')"
-      with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
+      with * have "x = y" and "x = y'"
+        by - (tactic "IntPr.fast_tac @{context} 1")+
       then have "y = y'" by (rule subst)
     } note r' = this
-    show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
+    show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'"
+      by (intro strip, elim conjE) (rule r')
   qed
 qed
 
-lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
+lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by (rule classical) iprover
 
-lemma swap: "~ P ==> (~ R ==> P) ==> R"
+lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
   by (rule classical) iprover
 
 
@@ -207,11 +215,11 @@
 \<close>
 
 
-lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
+lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
   by blast
 
-(* Elimination of True from asumptions: *)
-lemma True_implies_equals: "(True ==> PROP P) == PROP P"
+text \<open>Elimination of @{text True} from assumptions:\<close>
+lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
   assume "True \<Longrightarrow> PROP P"
   from this and TrueI show "PROP P" .
@@ -220,98 +228,108 @@
   then show "PROP P" .
 qed
 
-lemma uncurry: "P --> Q --> R ==> P & Q --> R"
+lemma uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
   by blast
 
-lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
+lemma iff_allI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
   by blast
 
-lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
+lemma iff_exI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
   by blast
 
-lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast
+lemma all_comm: "(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
+  by blast
 
-lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast
+lemma ex_comm: "(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
+  by blast
 
 
 
-(*** Classical simplification rules ***)
+subsection \<open>Classical simplification rules\<close>
 
-(*Avoids duplication of subgoals after expand_if, when the true and false
-  cases boil down to the same thing.*)
-lemma cases_simp: "(P --> Q) & (~P --> Q) <-> Q" by blast
+text \<open>
+  Avoids duplication of subgoals after @{text expand_if}, when the true and
+  false cases boil down to the same thing.
+\<close>
+
+lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
+  by blast
 
 
-(*** Miniscoping: pushing quantifiers in
-     We do NOT distribute of ALL over &, or dually that of EX over |
-     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
-     show that this step can increase proof length!
-***)
+subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
+
+text \<open>
+  We do NOT distribute of @{text "\<forall>"} over @{text "\<and>"}, or dually that of
+  @{text "\<exists>"} over @{text "\<or>"}.
 
-(*existential miniscoping*)
+  Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
+  this step can increase proof length!
+\<close>
+
+text \<open>Existential miniscoping.\<close>
 lemma int_ex_simps:
-  "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
-  "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
-  "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
-  "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
+  "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+  "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+  "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+  "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
   by iprover+
 
-(*classical rules*)
+text \<open>Classical rules.\<close>
 lemma cla_ex_simps:
-  "!!P Q. (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
-  "!!P Q. (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
+  "\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+  "\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
   by blast+
 
 lemmas ex_simps = int_ex_simps cla_ex_simps
 
-(*universal miniscoping*)
+text \<open>Universal miniscoping.\<close>
 lemma int_all_simps:
-  "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
-  "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
-  "!!P Q. (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
-  "!!P Q. (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
+  "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+  "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+  "\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q"
+  "\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
   by iprover+
 
-(*classical rules*)
+text \<open>Classical rules.\<close>
 lemma cla_all_simps:
-  "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
-  "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+  "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+  "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
   by blast+
 
 lemmas all_simps = int_all_simps cla_all_simps
 
 
-(*** Named rewrite rules proved for IFOL ***)
+subsubsection \<open>Named rewrite rules proved for IFOL\<close>
 
-lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast
-lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast
+lemma imp_disj1: "(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
+lemma imp_disj2: "Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
 
-lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast
+lemma de_Morgan_conj: "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)" by blast
 
-lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast
-lemma not_iff: "~(P <-> Q) <-> (P <-> ~Q)" by blast
+lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)" by blast
+lemma not_iff: "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
 
-lemma not_all: "(~ (ALL x. P(x))) <-> (EX x.~P(x))" by blast
-lemma imp_all: "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)" by blast
+lemma not_all: "(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))" by blast
+lemma imp_all: "((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)" by blast
 
 
 lemmas meta_simps =
-  triv_forall_equality (* prunes params *)
-  True_implies_equals  (* prune asms `True' *)
+  triv_forall_equality  -- \<open>prunes params\<close>
+  True_implies_equals  -- \<open>prune asms @{text True}\<close>
 
 lemmas IFOL_simps =
   refl [THEN P_iff_T] conj_simps disj_simps not_simps
   imp_simps iff_simps quant_simps
 
-lemma notFalseI: "~False" by iprover
+lemma notFalseI: "\<not> False" by iprover
 
 lemma cla_simps_misc:
-  "~(P&Q) <-> ~P | ~Q"
-  "P | ~P"
-  "~P | P"
-  "~ ~ P <-> P"
-  "(~P --> P) <-> P"
-  "(~P <-> ~Q) <-> (P<->Q)" by blast+
+  "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
+  "P \<or> \<not> P"
+  "\<not> P \<or> P"
+  "\<not> \<not> P \<longleftrightarrow> P"
+  "(\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
+  "(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)" by blast+
 
 lemmas cla_simps =
   de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
@@ -320,8 +338,8 @@
 
 ML_file "simpdata.ML"
 
-simproc_setup defined_Ex ("EX x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All ("ALL x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex ("\<exists>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
+simproc_setup defined_All ("\<forall>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
 
 ML \<open>
 (*intuitionistic simprules only*)
@@ -349,35 +367,36 @@
 
 subsection \<open>Other simple lemmas\<close>
 
-lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"
-by blast
+lemma [simp]: "((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)"
+  by blast
 
-lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
-by blast
+lemma [simp]: "((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))"
+  by blast
 
-lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
-by blast
+lemma not_disj_iff_imp: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)"
+  by blast
+
 
-(** Monotonicity of implications **)
+subsubsection \<open>Monotonicity of implications\<close>
 
-lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
+lemma conj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
+  by fast (*or (IntPr.fast_tac 1)*)
 
-lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
+lemma disj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)"
+  by fast (*or (IntPr.fast_tac 1)*)
 
-lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
+lemma imp_mono: "\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)"
+  by fast (*or (IntPr.fast_tac 1)*)
 
-lemma imp_refl: "P-->P"
-by (rule impI, assumption)
+lemma imp_refl: "P \<longrightarrow> P"
+  by (rule impI)
 
-(*The quantifier monotonicity rules are also intuitionistically valid*)
-lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))"
-by blast
+text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
+lemma ex_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
+  by blast
 
-lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))"
-by blast
+lemma all_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))"
+  by blast
 
 
 subsection \<open>Proof by cases and induction\<close>
diff -r 3590367b0ce9 -r f8cb97e0fd0b src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Oct 19 17:45:36 2015 +0200
+++ b/src/FOL/IFOL.thy	Mon Oct 19 20:29:29 2015 +0200
@@ -30,81 +30,85 @@
 typedecl o
 
 judgment
-  Trueprop      :: "o => prop"                  ("(_)" 5)
+  Trueprop :: "o \<Rightarrow> prop"  ("(_)" 5)
 
 
 subsubsection \<open>Equality\<close>
 
 axiomatization
-  eq :: "['a, 'a] => o"  (infixl "=" 50)
+  eq :: "['a, 'a] \<Rightarrow> o"  (infixl "=" 50)
 where
-  refl:         "a=a" and
-  subst:        "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
+  refl: "a = a" and
+  subst: "a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
 
 
 subsubsection \<open>Propositional logic\<close>
 
 axiomatization
   False :: o and
-  conj :: "[o, o] => o"  (infixr "&" 35) and
-  disj :: "[o, o] => o"  (infixr "|" 30) and
-  imp :: "[o, o] => o"  (infixr "-->" 25)
+  conj :: "[o, o] => o"  (infixr "\<and>" 35) and
+  disj :: "[o, o] => o"  (infixr "\<or>" 30) and
+  imp :: "[o, o] => o"  (infixr "\<longrightarrow>" 25)
 where
-  conjI: "[| P;  Q |] ==> P&Q" and
-  conjunct1: "P&Q ==> P" and
-  conjunct2: "P&Q ==> Q" and
+  conjI: "\<lbrakk>P;  Q\<rbrakk> \<Longrightarrow> P \<and> Q" and
+  conjunct1: "P \<and> Q \<Longrightarrow> P" and
+  conjunct2: "P \<and> Q \<Longrightarrow> Q" and
 
-  disjI1: "P ==> P|Q" and
-  disjI2: "Q ==> P|Q" and
-  disjE: "[| P|Q;  P ==> R;  Q ==> R |] ==> R" and
+  disjI1: "P \<Longrightarrow> P \<or> Q" and
+  disjI2: "Q \<Longrightarrow> P \<or> Q" and
+  disjE: "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" and
 
-  impI: "(P ==> Q) ==> P-->Q" and
-  mp: "[| P-->Q;  P |] ==> Q" and
+  impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
+  mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
 
-  FalseE: "False ==> P"
+  FalseE: "False \<Longrightarrow> P"
 
 
 subsubsection \<open>Quantifiers\<close>
 
 axiomatization
-  All :: "('a => o) => o"  (binder "ALL " 10) and
-  Ex :: "('a => o) => o"  (binder "EX " 10)
+  All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10) and
+  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
 where
-  allI: "(!!x. P(x)) ==> (ALL x. P(x))" and
-  spec: "(ALL x. P(x)) ==> P(x)" and
-  exI: "P(x) ==> (EX x. P(x))" and
-  exE: "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
+  allI: "(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))" and
+  spec: "(\<forall>x. P(x)) \<Longrightarrow> P(x)" and
+  exI: "P(x) \<Longrightarrow> (\<exists>x. P(x))" and
+  exE: "\<lbrakk>\<exists>x. P(x); \<And>x. P(x) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 
 
 subsubsection \<open>Definitions\<close>
 
-definition "True == False-->False"
-definition Not ("~ _" [40] 40) where not_def: "~P == P-->False"
-definition iff  (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)"
+definition "True \<equiv> False \<longrightarrow> False"
+
+definition Not ("\<not> _" [40] 40)
+  where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
 
-definition Ex1 :: "('a => o) => o"  (binder "EX! " 10)
-  where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+definition iff  (infixr "\<longleftrightarrow>" 25)
+  where "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
+
+definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>!" 10)
+  where ex1_def: "\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)"
 
 axiomatization where  -- \<open>Reflection, admissible\<close>
-  eq_reflection: "(x=y) ==> (x==y)" and
-  iff_reflection: "(P<->Q) ==> (P==Q)"
+  eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and
+  iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)"
+
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> o"  (infixl "\<noteq>" 50)
+  where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 
-subsubsection \<open>Additional notation\<close>
-
-abbreviation not_equal :: "['a, 'a] => o"  (infixl "~=" 50)
-  where "x ~= y == ~ (x = y)"
+subsubsection \<open>Old-style ASCII syntax\<close>
 
-notation (xsymbols)
-  not_equal  (infixl "\<noteq>" 50) and
-  Not  ("\<not> _" [40] 40) and
-  conj  (infixr "\<and>" 35) and
-  disj  (infixr "\<or>" 30) and
-  All  (binder "\<forall>" 10) and
-  Ex  (binder "\<exists>" 10) and
-  Ex1  (binder "\<exists>!" 10) and
-  imp  (infixr "\<longrightarrow>" 25) and
-  iff  (infixr "\<longleftrightarrow>" 25)
+notation (ASCII)
+  not_equal  (infixl "~=" 50) and
+  Not  ("~ _" [40] 40) and
+  conj  (infixr "&" 35) and
+  disj  (infixr "|" 30) and
+  All  (binder "ALL " 10) and
+  Ex  (binder "EX " 10) and
+  Ex1  (binder "EX! " 10) and
+  imp  (infixr "-->" 25) and
+  iff  (infixr "<->" 25)
 
 
 subsection \<open>Lemmas and proof tools\<close>
@@ -115,11 +119,11 @@
   unfolding True_def by (rule impI)
 
 
-(*** Sequent-style elimination rules for & --> and ALL ***)
+subsubsection \<open>Sequent-style elimination rules for @{text "\<and>"} @{text "\<longrightarrow>"} and @{text "\<forall>"}\<close>
 
 lemma conjE:
-  assumes major: "P & Q"
-    and r: "[| P; Q |] ==> R"
+  assumes major: "P \<and> Q"
+    and r: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   shows R
   apply (rule r)
    apply (rule major [THEN conjunct1])
@@ -127,9 +131,9 @@
   done
 
 lemma impE:
-  assumes major: "P --> Q"
+  assumes major: "P \<longrightarrow> Q"
     and P
-  and r: "Q ==> R"
+  and r: "Q \<Longrightarrow> R"
   shows R
   apply (rule r)
   apply (rule major [THEN mp])
@@ -137,17 +141,17 @@
   done
 
 lemma allE:
-  assumes major: "ALL x. P(x)"
-    and r: "P(x) ==> R"
+  assumes major: "\<forall>x. P(x)"
+    and r: "P(x) \<Longrightarrow> R"
   shows R
   apply (rule r)
   apply (rule major [THEN spec])
   done
 
-(*Duplicates the quantifier; for use with eresolve_tac*)
+text \<open>Duplicates the quantifier; for use with @{ML eresolve_tac}.\<close>
 lemma all_dupE:
-  assumes major: "ALL x. P(x)"
-    and r: "[| P(x); ALL x. P(x) |] ==> R"
+  assumes major: "\<forall>x. P(x)"
+    and r: "\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R"
   shows R
   apply (rule r)
    apply (rule major [THEN spec])
@@ -155,64 +159,71 @@
   done
 
 
-(*** Negation rules, which translate between ~P and P-->False ***)
+subsubsection \<open>Negation rules, which translate between @{text "\<not> P"} and @{text "P \<longrightarrow> False"}\<close>
 
-lemma notI: "(P ==> False) ==> ~P"
+lemma notI: "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P"
   unfolding not_def by (erule impI)
 
-lemma notE: "[| ~P;  P |] ==> R"
+lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R"
   unfolding not_def by (erule mp [THEN FalseE])
 
-lemma rev_notE: "[| P; ~P |] ==> R"
+lemma rev_notE: "\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R"
   by (erule notE)
 
-(*This is useful with the special implication rules for each kind of P. *)
+text \<open>This is useful with the special implication rules for each kind of @{text P}.\<close>
 lemma not_to_imp:
-  assumes "~P"
-    and r: "P --> False ==> Q"
+  assumes "\<not> P"
+    and r: "P \<longrightarrow> False \<Longrightarrow> Q"
   shows Q
   apply (rule r)
   apply (rule impI)
-  apply (erule notE [OF \<open>~P\<close>])
+  apply (erule notE [OF \<open>\<not> P\<close>])
   done
 
-(* For substitution into an assumption P, reduce Q to P-->Q, substitute into
-   this implication, then apply impI to move P back into the assumptions.*)
-lemma rev_mp: "[| P;  P --> Q |] ==> Q"
+text \<open>
+  For substitution into an assumption @{text P}, reduce @{text Q} to @{text
+  "P \<longrightarrow> Q"}, substitute into this implication, then apply @{text impI} to
+  move @{text P} back into the assumptions.
+\<close>
+lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   by (erule mp)
 
-(*Contrapositive of an inference rule*)
+text \<open>Contrapositive of an inference rule.\<close>
 lemma contrapos:
-  assumes major: "~Q"
-    and minor: "P ==> Q"
-  shows "~P"
+  assumes major: "\<not> Q"
+    and minor: "P \<Longrightarrow> Q"
+  shows "\<not> P"
   apply (rule major [THEN notE, THEN notI])
   apply (erule minor)
   done
 
 
-(*** Modus Ponens Tactics ***)
+subsubsection \<open>Modus Ponens Tactics\<close>
 
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+text \<open>
+  Finds @{text "P \<longrightarrow> Q"} and P in the assumptions, replaces implication by
+  @{text Q}.
+\<close>
 ML \<open>
-  fun mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i
-  fun eq_mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i
+  fun mp_tac ctxt i =
+    eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i;
+  fun eq_mp_tac ctxt i =
+    eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i;
 \<close>
 
 
-(*** If-and-only-if ***)
+subsection \<open>If-and-only-if\<close>
 
-lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q"
+lemma iffI: "\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q"
   apply (unfold iff_def)
   apply (rule conjI)
    apply (erule impI)
   apply (erule impI)
   done
 
-
 lemma iffE:
-  assumes major: "P <-> Q"
-    and r: "P-->Q ==> Q-->P ==> R"
+  assumes major: "P \<longleftrightarrow> Q"
+    and r: "P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> R"
   shows R
   apply (insert major, unfold iff_def)
   apply (erule conjE)
@@ -220,236 +231,250 @@
   apply assumption
   done
 
-(* Destruct rules for <-> similar to Modus Ponens *)
 
-lemma iffD1: "[| P <-> Q;  P |] ==> Q"
+subsubsection \<open>Destruct rules for @{text "\<longleftrightarrow>"} similar to Modus Ponens\<close>
+
+lemma iffD1: "\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q"
   apply (unfold iff_def)
   apply (erule conjunct1 [THEN mp])
   apply assumption
   done
 
-lemma iffD2: "[| P <-> Q;  Q |] ==> P"
+lemma iffD2: "\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P"
   apply (unfold iff_def)
   apply (erule conjunct2 [THEN mp])
   apply assumption
   done
 
-lemma rev_iffD1: "[| P; P <-> Q |] ==> Q"
+lemma rev_iffD1: "\<lbrakk>P; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   apply (erule iffD1)
   apply assumption
   done
 
-lemma rev_iffD2: "[| Q; P <-> Q |] ==> P"
+lemma rev_iffD2: "\<lbrakk>Q; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> P"
   apply (erule iffD2)
   apply assumption
   done
 
-lemma iff_refl: "P <-> P"
+lemma iff_refl: "P \<longleftrightarrow> P"
   by (rule iffI)
 
-lemma iff_sym: "Q <-> P ==> P <-> Q"
+lemma iff_sym: "Q \<longleftrightarrow> P \<Longrightarrow> P \<longleftrightarrow> Q"
   apply (erule iffE)
   apply (rule iffI)
   apply (assumption | erule mp)+
   done
 
-lemma iff_trans: "[| P <-> Q;  Q<-> R |] ==> P <-> R"
+lemma iff_trans: "\<lbrakk>P \<longleftrightarrow> Q; Q \<longleftrightarrow> R\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> R"
   apply (rule iffI)
   apply (assumption | erule iffE | erule (1) notE impE)+
   done
 
 
-(*** Unique existence.  NOTE THAT the following 2 quantifications
-   EX!x such that [EX!y such that P(x,y)]     (sequential)
-   EX!x,y such that P(x,y)                    (simultaneous)
- do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
-***)
+subsection \<open>Unique existence\<close>
+
+text \<open>
+  NOTE THAT the following 2 quantifications:
 
-lemma ex1I:
-  "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
+    \<^item> EX!x such that [EX!y such that P(x,y)]     (sequential)
+    \<^item> EX!x,y such that P(x,y)                    (simultaneous)
+
+  do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
+\<close>
+
+lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"
   apply (unfold ex1_def)
   apply (assumption | rule exI conjI allI impI)+
   done
 
-(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
-lemma ex_ex1I:
-  "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
+text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
+lemma ex_ex1I: "\<exists>x. P(x) \<Longrightarrow> (\<And>x y. \<lbrakk>P(x); P(y)\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> \<exists>!x. P(x)"
   apply (erule exE)
   apply (rule ex1I)
    apply assumption
   apply assumption
   done
 
-lemma ex1E:
-  "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
+lemma ex1E: "\<exists>! x. P(x) \<Longrightarrow> (\<And>x. \<lbrakk>P(x); \<forall>y. P(y) \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
   apply (unfold ex1_def)
   apply (assumption | erule exE conjE)+
   done
 
 
-(*** <-> congruence rules for simplification ***)
+subsubsection \<open>@{text "\<longleftrightarrow>"} congruence rules for simplification\<close>
 
-(*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
+text \<open>Use @{text iffE} on a premise. For @{text conj_cong}, @{text
+  imp_cong}, @{text all_cong}, @{text ex_cong}.\<close>
 ML \<open>
   fun iff_tac ctxt prems i =
     resolve_tac ctxt (prems RL @{thms iffE}) i THEN
-    REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i)
+    REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i);
 \<close>
 
 method_setup iff =
-  \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+  \<open>Attrib.thms >>
+    (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
 
 lemma conj_cong:
-  assumes "P <-> P'"
-    and "P' ==> Q <-> Q'"
-  shows "(P&Q) <-> (P'&Q')"
+  assumes "P \<longleftrightarrow> P'"
+    and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'"
+  shows "(P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
   apply (insert assms)
   apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
-(*Reversed congruence rule!   Used in ZF/Order*)
+text \<open>Reversed congruence rule!  Used in ZF/Order.\<close>
 lemma conj_cong2:
-  assumes "P <-> P'"
-    and "P' ==> Q <-> Q'"
-  shows "(Q&P) <-> (Q'&P')"
+  assumes "P \<longleftrightarrow> P'"
+    and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'"
+  shows "(Q \<and> P) \<longleftrightarrow> (Q' \<and> P')"
   apply (insert assms)
   apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 lemma disj_cong:
-  assumes "P <-> P'" and "Q <-> Q'"
-  shows "(P|Q) <-> (P'|Q')"
+  assumes "P \<longleftrightarrow> P'" and "Q \<longleftrightarrow> Q'"
+  shows "(P \<or> Q) \<longleftrightarrow> (P' \<or> Q')"
   apply (insert assms)
-  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+
+  apply (erule iffE disjE disjI1 disjI2 |
+    assumption | rule iffI | erule (1) notE impE)+
   done
 
 lemma imp_cong:
-  assumes "P <-> P'"
-    and "P' ==> Q <-> Q'"
-  shows "(P-->Q) <-> (P'-->Q')"
+  assumes "P \<longleftrightarrow> P'"
+    and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'"
+  shows "(P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
   apply (insert assms)
   apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
   done
 
-lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
+lemma iff_cong: "\<lbrakk>P \<longleftrightarrow> P'; Q \<longleftrightarrow> Q'\<rbrakk> \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P' \<longleftrightarrow> Q')"
   apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
   done
 
-lemma not_cong: "P <-> P' ==> ~P <-> ~P'"
+lemma not_cong: "P \<longleftrightarrow> P' \<Longrightarrow> \<not> P \<longleftrightarrow> \<not> P'"
   apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
   done
 
 lemma all_cong:
-  assumes "!!x. P(x) <-> Q(x)"
-  shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
+  assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)"
+  shows "(\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
   apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
   done
 
 lemma ex_cong:
-  assumes "!!x. P(x) <-> Q(x)"
-  shows "(EX x. P(x)) <-> (EX x. Q(x))"
+  assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)"
+  shows "(\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
   apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
   done
 
 lemma ex1_cong:
-  assumes "!!x. P(x) <-> Q(x)"
-  shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
+  assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)"
+  shows "(\<exists>!x. P(x)) \<longleftrightarrow> (\<exists>!x. Q(x))"
   apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
   done
 
-(*** Equality rules ***)
 
-lemma sym: "a=b ==> b=a"
+subsection \<open>Equality rules\<close>
+
+lemma sym: "a = b \<Longrightarrow> b = a"
   apply (erule subst)
   apply (rule refl)
   done
 
-lemma trans: "[| a=b;  b=c |] ==> a=c"
+lemma trans: "\<lbrakk>a = b; b = c\<rbrakk> \<Longrightarrow> a = c"
   apply (erule subst, assumption)
   done
 
-(**  **)
-lemma not_sym: "b ~= a ==> a ~= b"
+lemma not_sym: "b \<noteq> a \<Longrightarrow> a \<noteq> b"
   apply (erule contrapos)
   apply (erule sym)
   done
-  
-(* Two theorms for rewriting only one instance of a definition:
-   the first for definitions of formulae and the second for terms *)
 
-lemma def_imp_iff: "(A == B) ==> A <-> B"
+text \<open>
+  Two theorems for rewriting only one instance of a definition:
+  the first for definitions of formulae and the second for terms.
+\<close>
+
+lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> A \<longleftrightarrow> B"
   apply unfold
   apply (rule iff_refl)
   done
 
-lemma meta_eq_to_obj_eq: "(A == B) ==> A = B"
+lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> A = B"
   apply unfold
   apply (rule refl)
   done
 
-lemma meta_eq_to_iff: "x==y ==> x<->y"
+lemma meta_eq_to_iff: "x \<equiv> y \<Longrightarrow> x \<longleftrightarrow> y"
   by unfold (rule iff_refl)
 
-(*substitution*)
-lemma ssubst: "[| b = a; P(a) |] ==> P(b)"
+text \<open>Substitution.\<close>
+lemma ssubst: "\<lbrakk>b = a; P(a)\<rbrakk> \<Longrightarrow> P(b)"
   apply (drule sym)
   apply (erule (1) subst)
   done
 
-(*A special case of ex1E that would otherwise need quantifier expansion*)
-lemma ex1_equalsE:
-    "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
+text \<open>A special case of @{text ex1E} that would otherwise need quantifier
+  expansion.\<close>
+lemma ex1_equalsE: "\<lbrakk>\<exists>!x. P(x); P(a); P(b)\<rbrakk> \<Longrightarrow> a = b"
   apply (erule ex1E)
   apply (rule trans)
    apply (rule_tac [2] sym)
    apply (assumption | erule spec [THEN mp])+
   done
 
-(** Polymorphic congruence rules **)
 
-lemma subst_context: "[| a=b |]  ==>  t(a)=t(b)"
+subsubsection \<open>Polymorphic congruence rules\<close>
+
+lemma subst_context: "a = b \<Longrightarrow> t(a) = t(b)"
   apply (erule ssubst)
   apply (rule refl)
   done
 
-lemma subst_context2: "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
+lemma subst_context2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)"
+  apply (erule ssubst)+
+  apply (rule refl)
+  done
+
+lemma subst_context3: "\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)"
   apply (erule ssubst)+
   apply (rule refl)
   done
 
-lemma subst_context3: "[| a=b;  c=d;  e=f |]  ==>  t(a,c,e)=t(b,d,f)"
-  apply (erule ssubst)+
-  apply (rule refl)
-  done
+text \<open>
+  Useful with @{ML eresolve_tac} for proving equalties from known
+  equalities.
 
-(*Useful with eresolve_tac for proving equalties from known equalities.
         a = b
         |   |
-        c = d   *)
-lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
+        c = d
+\<close>
+lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
   apply (rule trans)
    apply (rule trans)
     apply (rule sym)
     apply assumption+
   done
 
-(*Dual of box_equals: for proving equalities backwards*)
-lemma simp_equals: "[| a=c;  b=d;  c=d |] ==> a=b"
+text \<open>Dual of box_equals: for proving equalities backwards.\<close>
+lemma simp_equals: "\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b"
   apply (rule trans)
    apply (rule trans)
     apply assumption+
   apply (erule sym)
   done
 
-(** Congruence rules for predicate letters **)
 
-lemma pred1_cong: "a=a' ==> P(a) <-> P(a')"
+subsubsection \<open>Congruence rules for predicate letters\<close>
+
+lemma pred1_cong: "a = a' \<Longrightarrow> P(a) \<longleftrightarrow> P(a')"
   apply (rule iffI)
    apply (erule (1) subst)
   apply (erule (1) ssubst)
   done
 
-lemma pred2_cong: "[| a=a';  b=b' |] ==> P(a,b) <-> P(a',b')"
+lemma pred2_cong: "\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> P(a,b) \<longleftrightarrow> P(a',b')"
   apply (rule iffI)
    apply (erule subst)+
    apply assumption
@@ -457,7 +482,7 @@
   apply assumption
   done
 
-lemma pred3_cong: "[| a=a';  b=b';  c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
+lemma pred3_cong: "\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> P(a,b,c) \<longleftrightarrow> P(a',b',c')"
   apply (rule iffI)
    apply (erule subst)+
    apply assumption
@@ -465,81 +490,85 @@
   apply assumption
   done
 
-(*special case for the equality predicate!*)
-lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'"
+text \<open>Special case for the equality predicate!\<close>
+lemma eq_cong: "\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> a = b \<longleftrightarrow> a' = b'"
   apply (erule (1) pred2_cong)
   done
 
 
-(*** Simplifications of assumed implications.
-     Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
-     used with mp_tac (restricted to atomic formulae) is COMPLETE for 
-     intuitionistic propositional logic.  See
-   R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
-    (preprint, University of St Andrews, 1991)  ***)
+subsection \<open>Simplifications of assumed implications\<close>
+
+text \<open>
+  Roy Dyckhoff has proved that @{text conj_impE}, @{text disj_impE}, and
+  @{text imp_impE} used with @{ML mp_tac} (restricted to atomic formulae) is
+  COMPLETE for intuitionistic propositional logic.
+
+  See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
+  (preprint, University of St Andrews, 1991).
+\<close>
 
 lemma conj_impE:
-  assumes major: "(P&Q)-->S"
-    and r: "P-->(Q-->S) ==> R"
+  assumes major: "(P \<and> Q) \<longrightarrow> S"
+    and r: "P \<longrightarrow> (Q \<longrightarrow> S) \<Longrightarrow> R"
   shows R
   by (assumption | rule conjI impI major [THEN mp] r)+
 
 lemma disj_impE:
-  assumes major: "(P|Q)-->S"
-    and r: "[| P-->S; Q-->S |] ==> R"
+  assumes major: "(P \<or> Q) \<longrightarrow> S"
+    and r: "\<lbrakk>P \<longrightarrow> S; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> R"
   shows R
   by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+
 
-(*Simplifies the implication.  Classical version is stronger. 
-  Still UNSAFE since Q must be provable -- backtracking needed.  *)
+text \<open>Simplifies the implication.  Classical version is stronger.
+  Still UNSAFE since Q must be provable -- backtracking needed.\<close>
 lemma imp_impE:
-  assumes major: "(P-->Q)-->S"
-    and r1: "[| P; Q-->S |] ==> Q"
-    and r2: "S ==> R"
+  assumes major: "(P \<longrightarrow> Q) \<longrightarrow> S"
+    and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q"
+    and r2: "S \<Longrightarrow> R"
   shows R
   by (assumption | rule impI major [THEN mp] r1 r2)+
 
-(*Simplifies the implication.  Classical version is stronger. 
-  Still UNSAFE since ~P must be provable -- backtracking needed.  *)
-lemma not_impE:
-  "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
+text \<open>Simplifies the implication.  Classical version is stronger.
+  Still UNSAFE since ~P must be provable -- backtracking needed.\<close>
+lemma not_impE: "\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R"
   apply (drule mp)
    apply (rule notI)
    apply assumption
   apply assumption
   done
 
-(*Simplifies the implication.   UNSAFE.  *)
+text \<open>Simplifies the implication. UNSAFE.\<close>
 lemma iff_impE:
-  assumes major: "(P<->Q)-->S"
-    and r1: "[| P; Q-->S |] ==> Q"
-    and r2: "[| Q; P-->S |] ==> P"
-    and r3: "S ==> R"
+  assumes major: "(P \<longleftrightarrow> Q) \<longrightarrow> S"
+    and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q"
+    and r2: "\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P"
+    and r3: "S \<Longrightarrow> R"
   shows R
   apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
   done
 
-(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
+text \<open>What if @{text "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"} is an assumption?
+  UNSAFE.\<close>
 lemma all_impE:
-  assumes major: "(ALL x. P(x))-->S"
-    and r1: "!!x. P(x)"
-    and r2: "S ==> R"
+  assumes major: "(\<forall>x. P(x)) \<longrightarrow> S"
+    and r1: "\<And>x. P(x)"
+    and r2: "S \<Longrightarrow> R"
   shows R
   apply (rule allI impI major [THEN mp] r1 r2)+
   done
 
-(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
+text \<open>
+  Unsafe: @{text "\<exists>x. P(x)) \<longrightarrow> S"} is equivalent
+  to @{text "\<forall>x. P(x) \<longrightarrow> S"}.\<close>
 lemma ex_impE:
-  assumes major: "(EX x. P(x))-->S"
-    and r: "P(x)-->S ==> R"
+  assumes major: "(\<exists>x. P(x)) \<longrightarrow> S"
+    and r: "P(x) \<longrightarrow> S \<Longrightarrow> R"
   shows R
   apply (assumption | rule exI impI major [THEN mp] r)+
   done
 
-(*** Courtesy of Krzysztof Grabczewski ***)
-
-lemma disj_imp_disj:
-  "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
+text \<open>Courtesy of Krzysztof Grabczewski.\<close>
+lemma disj_imp_disj: "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S"
   apply (erule disjE)
   apply (rule disjI1) apply assumption
   apply (rule disjI2) apply assumption
@@ -556,7 +585,7 @@
 
 ML_file "fologic.ML"
 
-lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
+lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
 
 ML \<open>
 structure Hypsubst = Hypsubst
@@ -583,9 +612,9 @@
 setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
 
 lemma impE':
-  assumes 1: "P --> Q"
-    and 2: "Q ==> R"
-    and 3: "P --> Q ==> P"
+  assumes 1: "P \<longrightarrow> Q"
+    and 2: "Q \<Longrightarrow> R"
+    and 3: "P \<longrightarrow> Q \<Longrightarrow> P"
   shows R
 proof -
   from 3 and 1 have P .
@@ -594,8 +623,8 @@
 qed
 
 lemma allE':
-  assumes 1: "ALL x. P(x)"
-    and 2: "P(x) ==> ALL x. P(x) ==> Q"
+  assumes 1: "\<forall>x. P(x)"
+    and 2: "P(x) \<Longrightarrow> \<forall>x. P(x) \<Longrightarrow> Q"
   shows Q
 proof -
   from 1 have "P(x)" by (rule spec)
@@ -603,8 +632,8 @@
 qed
 
 lemma notE':
-  assumes 1: "~ P"
-    and 2: "~ P ==> P"
+  assumes 1: "\<not> P"
+    and 2: "\<not> P \<Longrightarrow> P"
   shows R
 proof -
   from 2 and 1 have P .
@@ -616,70 +645,73 @@
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
-setup \<open>Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)\<close>
+setup \<open>
+  Context_Rules.addSWrapper
+    (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)
+\<close>
 
 
-lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
+lemma iff_not_sym: "\<not> (Q \<longleftrightarrow> P) \<Longrightarrow> \<not> (P \<longleftrightarrow> Q)"
   by iprover
 
 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
 
-lemma eq_commute: "a=b <-> b=a"
-apply (rule iffI) 
-apply (erule sym)+
-done
+lemma eq_commute: "a = b \<longleftrightarrow> b = a"
+  apply (rule iffI)
+  apply (erule sym)+
+  done
 
 
 subsection \<open>Atomizing meta-level rules\<close>
 
-lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
+lemma atomize_all [atomize]: "(\<And>x. P(x)) \<equiv> Trueprop (\<forall>x. P(x))"
 proof
-  assume "!!x. P(x)"
-  then show "ALL x. P(x)" ..
+  assume "\<And>x. P(x)"
+  then show "\<forall>x. P(x)" ..
 next
-  assume "ALL x. P(x)"
-  then show "!!x. P(x)" ..
+  assume "\<forall>x. P(x)"
+  then show "\<And>x. P(x)" ..
 qed
 
-lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
+lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
 proof
-  assume "A ==> B"
-  then show "A --> B" ..
+  assume "A \<Longrightarrow> B"
+  then show "A \<longrightarrow> B" ..
 next
-  assume "A --> B" and A
+  assume "A \<longrightarrow> B" and A
   then show B by (rule mp)
 qed
 
-lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
+lemma atomize_eq [atomize]: "(x \<equiv> y) \<equiv> Trueprop (x = y)"
 proof
-  assume "x == y"
-  show "x = y" unfolding \<open>x == y\<close> by (rule refl)
+  assume "x \<equiv> y"
+  show "x = y" unfolding \<open>x \<equiv> y\<close> by (rule refl)
 next
   assume "x = y"
-  then show "x == y" by (rule eq_reflection)
+  then show "x \<equiv> y" by (rule eq_reflection)
 qed
 
-lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
+lemma atomize_iff [atomize]: "(A \<equiv> B) \<equiv> Trueprop (A \<longleftrightarrow> B)"
 proof
-  assume "A == B"
-  show "A <-> B" unfolding \<open>A == B\<close> by (rule iff_refl)
+  assume "A \<equiv> B"
+  show "A \<longleftrightarrow> B" unfolding \<open>A \<equiv> B\<close> by (rule iff_refl)
 next
-  assume "A <-> B"
-  then show "A == B" by (rule iff_reflection)
+  assume "A \<longleftrightarrow> B"
+  then show "A \<equiv> B" by (rule iff_reflection)
 qed
 
-lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
+lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)"
 proof
   assume conj: "A &&& B"
-  show "A & B"
+  show "A \<and> B"
   proof (rule conjI)
     from conj show A by (rule conjunctionD1)
     from conj show B by (rule conjunctionD2)
   qed
 next
-  assume conj: "A & B"
+  assume conj: "A \<and> B"
   show "A &&& B"
   proof -
     from conj show A ..
@@ -693,24 +725,24 @@
 
 subsection \<open>Atomizing elimination rules\<close>
 
-lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
+lemma atomize_exL[atomize_elim]: "(\<And>x. P(x) \<Longrightarrow> Q) \<equiv> ((\<exists>x. P(x)) \<Longrightarrow> Q)"
   by rule iprover+
 
-lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
+lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
   by rule iprover+
 
-lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
+lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
   by rule iprover+
 
-lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
+lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop(A)" ..
 
 
 subsection \<open>Calculational rules\<close>
 
-lemma forw_subst: "a = b ==> P(b) ==> P(a)"
+lemma forw_subst: "a = b \<Longrightarrow> P(b) \<Longrightarrow> P(a)"
   by (rule ssubst)
 
-lemma back_subst: "P(a) ==> a = b ==> P(b)"
+lemma back_subst: "P(a) \<Longrightarrow> a = b \<Longrightarrow> P(b)"
   by (rule subst)
 
 text \<open>
@@ -724,12 +756,13 @@
   mp
   trans
 
+
 subsection \<open>``Let'' declarations\<close>
 
 nonterminal letbinds and letbind
 
-definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where
-    "Let(s, f) == f(s)"
+definition Let :: "['a::{}, 'a => 'b] \<Rightarrow> ('b::{})"
+  where "Let(s, f) \<equiv> f(s)"
 
 syntax
   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
@@ -739,12 +772,11 @@
 
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
-  "let x = a in e"          == "CONST Let(a, %x. e)"
-
+  "let x = a in e"          == "CONST Let(a, \<lambda>x. e)"
 
-lemma LetI: 
-  assumes "!!x. x=t ==> P(u(x))"
-  shows "P(let x=t in u(x))"
+lemma LetI:
+  assumes "\<And>x. x = t \<Longrightarrow> P(u(x))"
+  shows "P(let x = t in u(x))"
   apply (unfold Let_def)
   apply (rule refl [THEN assms])
   done
@@ -753,108 +785,113 @@
 subsection \<open>Intuitionistic simplification rules\<close>
 
 lemma conj_simps:
-  "P & True <-> P"
-  "True & P <-> P"
-  "P & False <-> False"
-  "False & P <-> False"
-  "P & P <-> P"
-  "P & P & Q <-> P & Q"
-  "P & ~P <-> False"
-  "~P & P <-> False"
-  "(P & Q) & R <-> P & (Q & R)"
+  "P \<and> True \<longleftrightarrow> P"
+  "True \<and> P \<longleftrightarrow> P"
+  "P \<and> False \<longleftrightarrow> False"
+  "False \<and> P \<longleftrightarrow> False"
+  "P \<and> P \<longleftrightarrow> P"
+  "P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
+  "P \<and> \<not> P \<longleftrightarrow> False"
+  "\<not> P \<and> P \<longleftrightarrow> False"
+  "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
   by iprover+
 
 lemma disj_simps:
-  "P | True <-> True"
-  "True | P <-> True"
-  "P | False <-> P"
-  "False | P <-> P"
-  "P | P <-> P"
-  "P | P | Q <-> P | Q"
-  "(P | Q) | R <-> P | (Q | R)"
+  "P \<or> True \<longleftrightarrow> True"
+  "True \<or> P \<longleftrightarrow> True"
+  "P \<or> False \<longleftrightarrow> P"
+  "False \<or> P \<longleftrightarrow> P"
+  "P \<or> P \<longleftrightarrow> P"
+  "P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
+  "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
   by iprover+
 
 lemma not_simps:
-  "~(P|Q)  <-> ~P & ~Q"
-  "~ False <-> True"
-  "~ True <-> False"
+  "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
+  "\<not> False \<longleftrightarrow> True"
+  "\<not> True \<longleftrightarrow> False"
   by iprover+
 
 lemma imp_simps:
-  "(P --> False) <-> ~P"
-  "(P --> True) <-> True"
-  "(False --> P) <-> True"
-  "(True --> P) <-> P"
-  "(P --> P) <-> True"
-  "(P --> ~P) <-> ~P"
+  "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+  "(P \<longrightarrow> True) \<longleftrightarrow> True"
+  "(False \<longrightarrow> P) \<longleftrightarrow> True"
+  "(True \<longrightarrow> P) \<longleftrightarrow> P"
+  "(P \<longrightarrow> P) \<longleftrightarrow> True"
+  "(P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
   by iprover+
 
 lemma iff_simps:
-  "(True <-> P) <-> P"
-  "(P <-> True) <-> P"
-  "(P <-> P) <-> True"
-  "(False <-> P) <-> ~P"
-  "(P <-> False) <-> ~P"
+  "(True \<longleftrightarrow> P) \<longleftrightarrow> P"
+  "(P \<longleftrightarrow> True) \<longleftrightarrow> P"
+  "(P \<longleftrightarrow> P) \<longleftrightarrow> True"
+  "(False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
+  "(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
   by iprover+
 
-(*The x=t versions are needed for the simplification procedures*)
+text \<open>The @{text "x = t"} versions are needed for the simplification
+  procedures.\<close>
 lemma quant_simps:
-  "!!P. (ALL x. P) <-> P"
-  "(ALL x. x=t --> P(x)) <-> P(t)"
-  "(ALL x. t=x --> P(x)) <-> P(t)"
-  "!!P. (EX x. P) <-> P"
-  "EX x. x=t"
-  "EX x. t=x"
-  "(EX x. x=t & P(x)) <-> P(t)"
-  "(EX x. t=x & P(x)) <-> P(t)"
+  "\<And>P. (\<forall>x. P) \<longleftrightarrow> P"
+  "(\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+  "(\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. (\<exists>x. P) \<longleftrightarrow> P"
+  "\<exists>x. x = t"
+  "\<exists>x. t = x"
+  "(\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
+  "(\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
   by iprover+
 
-(*These are NOT supplied by default!*)
+text \<open>These are NOT supplied by default!\<close>
 lemma distrib_simps:
-  "P & (Q | R) <-> P&Q | P&R"
-  "(Q | R) & P <-> Q&P | R&P"
-  "(P | Q --> R) <-> (P --> R) & (Q --> R)"
+  "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
+  "(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
+  "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
   by iprover+
 
 
-text \<open>Conversion into rewrite rules\<close>
+subsubsection \<open>Conversion into rewrite rules\<close>
 
-lemma P_iff_F: "~P ==> (P <-> False)" by iprover
-lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection])
+lemma P_iff_F: "\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)"
+  by iprover
+lemma iff_reflection_F: "\<not> P \<Longrightarrow> (P \<equiv> False)"
+  by (rule P_iff_F [THEN iff_reflection])
 
-lemma P_iff_T: "P ==> (P <-> True)" by iprover
-lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection])
+lemma P_iff_T: "P \<Longrightarrow> (P \<longleftrightarrow> True)"
+  by iprover
+lemma iff_reflection_T: "P \<Longrightarrow> (P \<equiv> True)"
+  by (rule P_iff_T [THEN iff_reflection])
 
 
-text \<open>More rewrite rules\<close>
+subsubsection \<open>More rewrite rules\<close>
 
-lemma conj_commute: "P&Q <-> Q&P" by iprover
-lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover
+lemma conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P" by iprover
+lemma conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover
 lemmas conj_comms = conj_commute conj_left_commute
 
-lemma disj_commute: "P|Q <-> Q|P" by iprover
-lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover
+lemma disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P" by iprover
+lemma disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover
 lemmas disj_comms = disj_commute disj_left_commute
 
-lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover
-lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover
+lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)" by iprover
+lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)" by iprover
 
-lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover
-lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover
+lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
+lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
 
-lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover
-lemma imp_conj: "((P&Q)-->R)   <-> (P --> (Q --> R))" by iprover
-lemma imp_disj: "(P|Q --> R)   <-> (P-->R) & (Q-->R)" by iprover
+lemma imp_conj_distrib: "(P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" by iprover
+lemma imp_conj: "((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
+lemma imp_disj: "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)" by iprover
 
-lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover
+lemma de_Morgan_disj: "(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)" by iprover
 
-lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover
-lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover
+lemma not_ex: "(\<not> (\<exists>x. P(x))) \<longleftrightarrow> (\<forall>x. \<not> P(x))" by iprover
+lemma imp_ex: "((\<exists>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> Q)" by iprover
 
-lemma ex_disj_distrib:
-  "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover
+lemma ex_disj_distrib: "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> ((\<exists>x. P(x)) \<or> (\<exists>x. Q(x)))"
+  by iprover
 
-lemma all_conj_distrib:
-  "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
+lemma all_conj_distrib: "(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))"
+  by iprover
 
 end
diff -r 3590367b0ce9 -r f8cb97e0fd0b src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Oct 19 17:45:36 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Oct 19 20:29:29 2015 +0200
@@ -162,8 +162,8 @@
 declare [[show_hyps]]
 
 ML \<open>
-  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
-  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+  check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
 \<close>
 
 end
@@ -175,8 +175,8 @@
   (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
 
 ML \<open>
-  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
-  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) \<longleftrightarrow> \<not> p2(p3(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
 \<close>
 
 end