# HG changeset patch
# User wenzelm
# Date 1451641740 -3600
# Node ID 5d208fd2507d07bb9f64ff0e40c61bf3f1b3b3b9
# Parent  9de1eb745aebd614e12354e0c5e24c019bd30d99
isabelle update_cartouches -c -t;

diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/CCL.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -303,7 +303,7 @@
   and [dest!] = ccl_injDs
 
 
-subsection \<open>Facts from gfp Definition of @{text "[="} and @{text "="}\<close>
+subsection \<open>Facts from gfp Definition of \<open>[=\<close> and \<open>=\<close>\<close>
 
 lemma XHlemma1: "\<lbrakk>A=B; a:B \<longleftrightarrow> P\<rbrakk> \<Longrightarrow> a:A \<longleftrightarrow> P"
   by simp
@@ -422,7 +422,7 @@
 lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1
 
 
-subsection \<open>Coinduction for @{text "[="}\<close>
+subsection \<open>Coinduction for \<open>[=\<close>\<close>
 
 lemma po_coinduct: "\<lbrakk><t,u> : R; R <= POgen(R)\<rbrakk> \<Longrightarrow> t [= u"
   apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]])
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Gfp.thy
--- a/src/CCL/Gfp.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Gfp.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -10,7 +10,7 @@
 begin
 
 definition
-  gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where -- "greatest fixed point"
+  gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> "greatest fixed point"
   "gfp(f) == Union({u. u <= f(u)})"
 
 (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
@@ -90,7 +90,7 @@
   done
 
 
-subsection \<open>Definition forms of @{text "gfp_Tarski"}, to control unfolding\<close>
+subsection \<open>Definition forms of \<open>gfp_Tarski\<close>, to control unfolding\<close>
 
 lemma def_gfp_Tarski: "\<lbrakk>h == gfp(f); mono(f)\<rbrakk> \<Longrightarrow> h = f(h)"
   apply unfold
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Hered.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -10,8 +10,8 @@
 begin
 
 text \<open>
-  Note that this is based on an untyped equality and so @{text "lam
-  x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"}
+  Note that this is based on an untyped equality and so \<open>lam
+  x. b(x)\<close> is only hereditarily terminating if \<open>ALL x. b(x)\<close>
   is.  Not so useful for functions!
 \<close>
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Lfp.thy
--- a/src/CCL/Lfp.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Lfp.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -10,7 +10,7 @@
 begin
 
 definition
-  lfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where -- "least fixed point"
+  lfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where \<comment> "least fixed point"
   "lfp(f) == Inter({u. f(u) <= u})"
 
 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Set.thy
--- a/src/CCL/Set.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Set.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -411,7 +411,7 @@
   by (blast intro: equalityI elim: equalityE)
 
 
-subsection \<open>Simple properties of @{text "Compl"} -- complement of a set\<close>
+subsection \<open>Simple properties of \<open>Compl\<close> -- complement of a set\<close>
 
 lemma Compl_disjoint: "A Int Compl(A) = {x. False}"
   by (blast intro: equalityI)
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Term.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -291,7 +291,7 @@
 \<close>
 
 
-subsection \<open>Rules for pre-order @{text "[="}\<close>
+subsection \<open>Rules for pre-order \<open>[=\<close>\<close>
 
 lemma term_porews:
   "inl(a) [= inl(a') \<longleftrightarrow> a [= a'"
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Trancl.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -25,7 +25,7 @@
   where "r^+ == r O rtrancl(r)"
 
 
-subsection \<open>Natural deduction for @{text "trans(r)"}\<close>
+subsection \<open>Natural deduction for \<open>trans(r)\<close>\<close>
 
 lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)"
   unfolding trans_def by blast
diff -r 9de1eb745aeb -r 5d208fd2507d src/CCL/Type.thy
--- a/src/CCL/Type.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/CCL/Type.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -364,8 +364,7 @@
   done
 
 
-subsection \<open>Lemmas and tactics for using the rule @{text
-  "coinduct3"} on @{text "[="} and @{text "="}\<close>
+subsection \<open>Lemmas and tactics for using the rule \<open>coinduct3\<close> on \<open>[=\<close> and \<open>=\<close>\<close>
 
 lemma lfpI: "\<lbrakk>mono(f); a : f(lfp(f))\<rbrakk> \<Longrightarrow> a : lfp(f)"
   apply (erule lfp_Tarski [THEN ssubst])
diff -r 9de1eb745aeb -r 5d208fd2507d src/Cube/Example.thy
--- a/src/Cube/Example.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/Cube/Example.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -149,7 +149,7 @@
 
 schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
     ?p: (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P"
-  -- \<open>Antisymmetry implies irreflexivity:\<close>
+  \<comment> \<open>Antisymmetry implies irreflexivity:\<close>
   apply (strip_asms rules)
   apply (rule lam_ss)
     apply (depth_solve1 rules)
@@ -206,7 +206,7 @@
 
 schematic_goal (in LP2)
   "A:* a:A b:A \<turnstile> ?p: (\<Prod>P:A\<rightarrow>*.P\<cdot>a\<rightarrow>P\<cdot>b) \<rightarrow> (\<Prod>P:A\<rightarrow>*.P\<cdot>b\<rightarrow>P\<cdot>a)"
-  -- \<open>Symmetry of Leibnitz equality\<close>
+  \<comment> \<open>Symmetry of Leibnitz equality\<close>
   apply (strip_asms rules)
   apply (rule lam_ss)
     apply (depth_solve1 rules)
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/FOL.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -26,7 +26,7 @@
   by (erule FalseE [THEN classical])
 
 
-subsubsection \<open>Classical introduction rules for @{text "\<or>"} and @{text "\<exists>"}\<close>
+subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close>
 
 lemma disjCI: "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"
   apply (rule classical)
@@ -34,7 +34,7 @@
   apply (erule notE disjI2)+
   done
 
-text \<open>Introduction rule involving only @{text "\<exists>"}\<close>
+text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close>
 lemma ex_classical:
   assumes r: "\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)"
   shows "\<exists>x. P(x)"
@@ -42,7 +42,7 @@
   apply (rule exI, erule r)
   done
 
-text \<open>Version of above, simplifying @{text "\<not>\<exists>"} to @{text "\<forall>\<not>"}.\<close>
+text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close>
 lemma exCI:
   assumes r: "\<forall>x. \<not> P(x) \<Longrightarrow> P(a)"
   shows "\<exists>x. P(x)"
@@ -79,7 +79,7 @@
 
 subsection \<open>Special elimination rules\<close>
 
-text \<open>Classical implies (@{text "\<longrightarrow>"}) elimination.\<close>
+text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
 lemma impCE:
   assumes major: "P \<longrightarrow> Q"
     and r1: "\<not> P \<Longrightarrow> R"
@@ -92,8 +92,7 @@
   done
 
 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''.
+  This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for those cases in which P holds ``almost everywhere''.
   Can't install as default: would break old proofs.
 \<close>
 lemma impCE':
@@ -124,8 +123,8 @@
 subsubsection \<open>Tactics for implication and contradiction\<close>
 
 text \<open>
-  Classical @{text "\<longleftrightarrow>"} elimination. Proof substitutes @{text "P = Q"} in
-  @{text "\<not> P \<Longrightarrow> \<not> Q"} and @{text "P \<Longrightarrow> Q"}.
+  Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in
+  \<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>.
 \<close>
 lemma iffCE:
   assumes major: "P \<longleftrightarrow> Q"
@@ -218,7 +217,7 @@
 lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
   by blast
 
-text \<open>Elimination of @{text True} from assumptions:\<close>
+text \<open>Elimination of \<open>True\<close> from assumptions:\<close>
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
 proof
   assume "True \<Longrightarrow> PROP P"
@@ -248,7 +247,7 @@
 subsection \<open>Classical simplification rules\<close>
 
 text \<open>
-  Avoids duplication of subgoals after @{text expand_if}, when the true and
+  Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and
   false cases boil down to the same thing.
 \<close>
 
@@ -259,8 +258,8 @@
 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>"}.
+  We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of
+  \<open>\<exists>\<close> over \<open>\<or>\<close>.
 
   Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
   this step can increase proof length!
@@ -314,8 +313,8 @@
 
 
 lemmas meta_simps =
-  triv_forall_equality  -- \<open>prunes params\<close>
-  True_implies_equals  -- \<open>prune asms @{text True}\<close>
+  triv_forall_equality  \<comment> \<open>prunes params\<close>
+  True_implies_equals  \<comment> \<open>prune asms \<open>True\<close>\<close>
 
 lemmas IFOL_simps =
   refl [THEN P_iff_T] conj_simps disj_simps not_simps
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/IFOL.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -89,7 +89,7 @@
 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>
+axiomatization where  \<comment> \<open>Reflection, admissible\<close>
   eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and
   iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)"
 
@@ -119,7 +119,7 @@
   unfolding True_def by (rule impI)
 
 
-subsubsection \<open>Sequent-style elimination rules for @{text "\<and>"} @{text "\<longrightarrow>"} and @{text "\<forall>"}\<close>
+subsubsection \<open>Sequent-style elimination rules for \<open>\<and>\<close> \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close>\<close>
 
 lemma conjE:
   assumes major: "P \<and> Q"
@@ -159,7 +159,7 @@
   done
 
 
-subsubsection \<open>Negation rules, which translate between @{text "\<not> P"} and @{text "P \<longrightarrow> False"}\<close>
+subsubsection \<open>Negation rules, which translate between \<open>\<not> P\<close> and \<open>P \<longrightarrow> False\<close>\<close>
 
 lemma notI: "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P"
   unfolding not_def by (erule impI)
@@ -170,7 +170,7 @@
 lemma rev_notE: "\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R"
   by (erule notE)
 
-text \<open>This is useful with the special implication rules for each kind of @{text P}.\<close>
+text \<open>This is useful with the special implication rules for each kind of \<open>P\<close>.\<close>
 lemma not_to_imp:
   assumes "\<not> P"
     and r: "P \<longrightarrow> False \<Longrightarrow> Q"
@@ -181,9 +181,8 @@
   done
 
 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.
+  For substitution into an assumption \<open>P\<close>, reduce \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, substitute into this implication, then apply \<open>impI\<close> to
+  move \<open>P\<close> back into the assumptions.
 \<close>
 lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   by (erule mp)
@@ -201,8 +200,8 @@
 subsubsection \<open>Modus Ponens Tactics\<close>
 
 text \<open>
-  Finds @{text "P \<longrightarrow> Q"} and P in the assumptions, replaces implication by
-  @{text Q}.
+  Finds \<open>P \<longrightarrow> Q\<close> and P in the assumptions, replaces implication by
+  \<open>Q\<close>.
 \<close>
 ML \<open>
   fun mp_tac ctxt i =
@@ -232,7 +231,7 @@
   done
 
 
-subsubsection \<open>Destruct rules for @{text "\<longleftrightarrow>"} similar to Modus Ponens\<close>
+subsubsection \<open>Destruct rules for \<open>\<longleftrightarrow>\<close> similar to Modus Ponens\<close>
 
 lemma iffD1: "\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q"
   apply (unfold iff_def)
@@ -301,10 +300,9 @@
   done
 
 
-subsubsection \<open>@{text "\<longleftrightarrow>"} congruence rules for simplification\<close>
+subsubsection \<open>\<open>\<longleftrightarrow>\<close> congruence rules for simplification\<close>
 
-text \<open>Use @{text iffE} on a premise. For @{text conj_cong}, @{text
-  imp_cong}, @{text all_cong}, @{text ex_cong}.\<close>
+text \<open>Use \<open>iffE\<close> on a premise. For \<open>conj_cong\<close>, \<open>imp_cong\<close>, \<open>all_cong\<close>, \<open>ex_cong\<close>.\<close>
 ML \<open>
   fun iff_tac ctxt prems i =
     resolve_tac ctxt (prems RL @{thms iffE}) i THEN
@@ -415,7 +413,7 @@
   apply (erule (1) subst)
   done
 
-text \<open>A special case of @{text ex1E} that would otherwise need quantifier
+text \<open>A special case of \<open>ex1E\<close> 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)
@@ -457,7 +455,7 @@
     apply assumption+
   done
 
-text \<open>Dual of @{text box_equals}: for proving equalities backwards.\<close>
+text \<open>Dual of \<open>box_equals\<close>: 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)
@@ -499,8 +497,8 @@
 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
+  Roy Dyckhoff has proved that \<open>conj_impE\<close>, \<open>disj_impE\<close>, and
+  \<open>imp_impE\<close> 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
@@ -547,7 +545,7 @@
   apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
   done
 
-text \<open>What if @{text "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"} is an assumption?
+text \<open>What if \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close> is an assumption?
   UNSAFE.\<close>
 lemma all_impE:
   assumes major: "(\<forall>x. P(x)) \<longrightarrow> S"
@@ -558,8 +556,8 @@
   done
 
 text \<open>
-  Unsafe: @{text "\<exists>x. P(x)) \<longrightarrow> S"} is equivalent
-  to @{text "\<forall>x. P(x) \<longrightarrow> S"}.\<close>
+  Unsafe: \<open>\<exists>x. P(x)) \<longrightarrow> S\<close> is equivalent
+  to \<open>\<forall>x. P(x) \<longrightarrow> S\<close>.\<close>
 lemma ex_impE:
   assumes major: "(\<exists>x. P(x)) \<longrightarrow> S"
     and r: "P(x) \<longrightarrow> S \<Longrightarrow> R"
@@ -829,7 +827,7 @@
   "(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
   by iprover+
 
-text \<open>The @{text "x = t"} versions are needed for the simplification
+text \<open>The \<open>x = t\<close> versions are needed for the simplification
   procedures.\<close>
 lemma quant_simps:
   "\<And>P. (\<forall>x. P) \<longleftrightarrow> P"
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Classical.thy
--- a/src/FOL/ex/Classical.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Classical.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -321,9 +321,9 @@
   by blast
 
 text \<open>
-  Other proofs: Can use @{text auto}, which cheats by using rewriting!
-  @{text Deepen_tac} alone requires 253 secs.  Or
-  @{text \<open>by (mini_tac 1 THEN Deepen_tac 5 1)\<close>}.
+  Other proofs: Can use \<open>auto\<close>, which cheats by using rewriting!
+  \<open>Deepen_tac\<close> alone requires 253 secs.  Or
+  \<open>by (mini_tac 1 THEN Deepen_tac 5 1)\<close>.
 \<close>
 
 text\<open>44\<close>
@@ -366,7 +366,7 @@
   apply safe
   apply (rule_tac x = a in allE, assumption)
   apply (rule_tac x = b in allE, assumption)
-  apply fast  -- \<open>blast's treatment of equality can't do it\<close>
+  apply fast  \<comment> \<open>blast's treatment of equality can't do it\<close>
   done
 
 text\<open>50. (What has this to do with equality?)\<close>
@@ -399,7 +399,7 @@
    (\<forall>x. hates(agatha,x) \<longrightarrow> hates(butler,x)) \<and>
    (\<forall>x. \<not> hates(x,agatha) \<or> \<not> hates(x,butler) \<or> \<not> hates(x,charles)) \<longrightarrow>
     killed(?who,agatha)"
-  by fast  -- \<open>MUCH faster than blast\<close>
+  by fast  \<comment> \<open>MUCH faster than blast\<close>
 
 
 text\<open>56\<close>
@@ -468,7 +468,7 @@
                     ((C(y) \<and> Q(w,y,y)) \<and> OO(w,b) \<longrightarrow> P(v,y) \<and> OO(v,b)))))
      \<longrightarrow> \<not> (\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z))))"
   by (blast 12)
-    -- \<open>Needed because the search for depths below 12 is very slow.\<close>
+    \<comment> \<open>Needed because the search for depths below 12 is very slow.\<close>
 
 
 text \<open>
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/If.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -26,7 +26,7 @@
   apply (rule ifI)
   oops
 
-text\<open>Trying again from the beginning in order to use @{text blast}\<close>
+text\<open>Trying again from the beginning in order to use \<open>blast\<close>\<close>
 declare ifI [intro!]
 declare ifE [elim!]
 
@@ -45,7 +45,7 @@
 text \<open>An invalid formula. High-level rules permit a simpler diagnosis.\<close>
 lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))"
   apply auto
-    -- \<open>The next step will fail unless subgoals remain\<close>
+    \<comment> \<open>The next step will fail unless subgoals remain\<close>
   apply (tactic all_tac)
   oops
 
@@ -53,7 +53,7 @@
 lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))"
   unfolding if_def
   apply auto
-    -- \<open>The next step will fail unless subgoals remain\<close>
+    \<comment> \<open>The next step will fail unless subgoals remain\<close>
   apply (tactic all_tac)
   oops
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Intro.thy
--- a/src/FOL/ex/Intro.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Intro.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -30,7 +30,7 @@
 apply assumption+
 done
 
-text \<open>Correct version, delaying use of @{text spec} until last.\<close>
+text \<open>Correct version, delaying use of \<open>spec\<close> until last.\<close>
 lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))"
 apply (rule impI)
 apply (rule allI)
@@ -41,7 +41,7 @@
 done
 
 
-subsubsection \<open>Demonstration of @{text "fast"}\<close>
+subsubsection \<open>Demonstration of \<open>fast\<close>\<close>
 
 lemma "(\<exists>y. \<forall>x. J(y,x) \<longleftrightarrow> \<not> J(x,x)) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. J(z,y) \<longleftrightarrow> \<not> J(z,x))"
 apply fast
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Intuitionistic.thy
--- a/src/FOL/ex/Intuitionistic.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Intuitionistic.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -82,12 +82,12 @@
   The attempt to prove them terminates quickly!\<close>
 lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
 oops
 
 lemma "(P \<and> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> R) \<or> (Q \<longrightarrow> R)"
 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
 oops
 
 
@@ -121,7 +121,7 @@
 lemma
   "(\<forall>x. \<exists>y. \<forall>z. p(x) \<and> q(y) \<and> r(z)) \<longleftrightarrow>
     (\<forall>z. \<exists>y. \<forall>x. p(x) \<and> q(y) \<and> r(z))"
-  by (tactic \<open>IntPr.best_dup_tac @{context} 1\<close>)  --\<open>SLOW\<close>
+  by (tactic \<open>IntPr.best_dup_tac @{context} 1\<close>)  \<comment>\<open>SLOW\<close>
 
 text\<open>Problem 3.1\<close>
 lemma "\<not> (\<exists>x. \<forall>y. mem(y,x) \<longleftrightarrow> \<not> mem(x,x))"
@@ -136,11 +136,11 @@
 
 subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
 
-text\<open>@{text "\<not>\<not>"}1\<close>
+text\<open>\<open>\<not>\<not>\<close>1\<close>
 lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}2\<close>
+text\<open>\<open>\<not>\<not>\<close>2\<close>
 lemma "\<not> \<not> (\<not> \<not> P \<longleftrightarrow> P)"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
@@ -148,23 +148,23 @@
 lemma "\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}4\<close>
+text\<open>\<open>\<not>\<not>\<close>4\<close>
 lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}5\<close>
+text\<open>\<open>\<not>\<not>\<close>5\<close>
 lemma "\<not> \<not> ((P \<or> Q \<longrightarrow> P \<or> R) \<longrightarrow> P \<or> (Q \<longrightarrow> R))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}6\<close>
+text\<open>\<open>\<not>\<not>\<close>6\<close>
 lemma "\<not> \<not> (P \<or> \<not> P)"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}7\<close>
+text\<open>\<open>\<not>\<not>\<close>7\<close>
 lemma "\<not> \<not> (P \<or> \<not> \<not> \<not> P)"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}8. Peirce's law\<close>
+text\<open>\<open>\<not>\<not>\<close>8. Peirce's law\<close>
 lemma "\<not> \<not> (((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P)"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
@@ -182,7 +182,7 @@
 lemma "P \<longleftrightarrow> P"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}12. Dijkstra's law\<close>
+text\<open>\<open>\<not>\<not>\<close>12. Dijkstra's law\<close>
 lemma "\<not> \<not> (((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R)))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
@@ -193,19 +193,19 @@
 lemma "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}14\<close>
+text\<open>\<open>\<not>\<not>\<close>14\<close>
 lemma "\<not> \<not> ((P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P)))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}15\<close>
+text\<open>\<open>\<not>\<not>\<close>15\<close>
 lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}16\<close>
+text\<open>\<open>\<not>\<not>\<close>16\<close>
 lemma "\<not> \<not> ((P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}17\<close>
+text\<open>\<open>\<not>\<not>\<close>17\<close>
 lemma "\<not> \<not> (((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S)))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
@@ -239,28 +239,28 @@
 
 lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)"
   apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
   oops
 
 lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<longrightarrow> (\<exists>x. P \<longrightarrow> Q(x))"
   apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
   oops
 
 lemma "(\<forall>x. P(x) \<or> Q) \<longrightarrow> ((\<forall>x. P(x)) \<or> Q)"
   apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
   oops
 
 lemma "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"
   apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
   oops
 
 text \<open>Classically but not intuitionistically valid.  Proved by a bug in 1986!\<close>
 lemma "\<exists>x. Q(x) \<longrightarrow> (\<forall>x. Q(x))"
   apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
-  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
   oops
 
 
@@ -271,13 +271,13 @@
   require quantifier duplication -- not currently available.
 \<close>
 
-text\<open>@{text "\<not>\<not>"}18\<close>
+text\<open>\<open>\<not>\<not>\<close>18\<close>
 lemma "\<not> \<not> (\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x))"
-  oops  -- \<open>NOT PROVED\<close>
+  oops  \<comment> \<open>NOT PROVED\<close>
 
-text\<open>@{text "\<not>\<not>"}19\<close>
+text\<open>\<open>\<not>\<not>\<close>19\<close>
 lemma "\<not> \<not> (\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x)))"
-  oops  -- \<open>NOT PROVED\<close>
+  oops  \<comment> \<open>NOT PROVED\<close>
 
 text\<open>20\<close>
 lemma
@@ -287,13 +287,13 @@
 
 text\<open>21\<close>
 lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> \<not> \<not> (\<exists>x. P \<longleftrightarrow> Q(x))"
-  oops -- \<open>NOT PROVED; needs quantifier duplication\<close>
+  oops \<comment> \<open>NOT PROVED; needs quantifier duplication\<close>
 
 text\<open>22\<close>
 lemma "(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}23\<close>
+text\<open>\<open>\<not>\<not>\<close>23\<close>
 lemma "\<not> \<not> ((\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x))))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
@@ -303,8 +303,8 @@
     (\<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
     \<longrightarrow> \<not> \<not> (\<exists>x. P(x) \<and> R(x))"
 text \<open>
-  Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and
-  @{text ITER_DEEPEN} all take forever.
+  Not clear why \<open>fast_tac\<close>, \<open>best_tac\<close>, \<open>ASTAR\<close> and
+  \<open>ITER_DEEPEN\<close> all take forever.
 \<close>
   apply (tactic \<open>IntPr.safe_tac @{context}\<close>)
   apply (erule impE)
@@ -321,12 +321,12 @@
     \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}26\<close>
+text\<open>\<open>\<not>\<not>\<close>26\<close>
 lemma
   "(\<not> \<not> (\<exists>x. p(x)) \<longleftrightarrow> \<not> \<not> (\<exists>x. q(x))) \<and>
     (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
   \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))"
-  oops  --\<open>NOT PROVED\<close>
+  oops  \<comment>\<open>NOT PROVED\<close>
 
 text\<open>27\<close>
 lemma
@@ -337,7 +337,7 @@
   \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}28. AMENDED\<close>
+text\<open>\<open>\<not>\<not>\<close>28. AMENDED\<close>
 lemma
   "(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
       (\<not> \<not> (\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
@@ -352,7 +352,7 @@
       (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}30\<close>
+text\<open>\<open>\<not>\<not>\<close>30\<close>
 lemma
   "(\<forall>x. (P(x) \<or> Q(x)) \<longrightarrow> \<not> R(x)) \<and>
       (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
@@ -375,7 +375,7 @@
   \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>@{text "\<not>\<not>"}33\<close>
+text\<open>\<open>\<not>\<not>\<close>33\<close>
 lemma
   "(\<forall>x. \<not> \<not> (P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c))) \<longleftrightarrow>
     (\<forall>x. \<not> \<not> ((\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c))))"
@@ -398,7 +398,7 @@
         (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
         (\<not> \<not> (\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
     \<longrightarrow> \<not> \<not> (\<forall>x. \<exists>y. R(x,y))"
-  oops  --\<open>NOT PROVED\<close>
+  oops  \<comment>\<open>NOT PROVED\<close>
 
 text\<open>39\<close>
 lemma "\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -86,7 +86,7 @@
 locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
 print_locale! pert_hom thm pert_hom_def
 
-text \<open>Alternative expression, obtaining nicer names in @{text "semi f"}.\<close>
+text \<open>Alternative expression, obtaining nicer names in \<open>semi f\<close>.\<close>
 locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
 print_locale! pert_hom' thm pert_hom'_def
 
@@ -731,12 +731,12 @@
 proof -
   show "dgrp(prod)" by unfold_locales
   from this interpret d: dgrp .
-  -- Unit
+  \<comment> Unit
   have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
   also have "... = glob_one(prod) ** one" by (simp add: rone)
   also have "... = one" by (simp add: glob_lone)
   finally show "dgrp.one(prod) = one" .
-  -- Inverse
+  \<comment> Inverse
   then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
   then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
 qed
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Nat_Class.thy
--- a/src/FOL/ex/Nat_Class.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Nat_Class.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -7,11 +7,11 @@
 begin
 
 text \<open>
-  This is an abstract version of theory @{text Nat}. Instead of
-  axiomatizing a single type @{text nat} we define the class of all
+  This is an abstract version of theory \<open>Nat\<close>. Instead of
+  axiomatizing a single type \<open>nat\<close> we define the class of all
   these types (up to isomorphism).
 
-  Note: The @{text rec} operator had to be made \emph{monomorphic},
+  Note: The \<open>rec\<close> operator had to be made \emph{monomorphic},
   because class axioms may not contain more than one type variable.
 \<close>
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Prolog.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -56,7 +56,7 @@
 done
 
 schematic_goal "rev(?x, a:b:c:Nil)"
-apply (rule rules)+  -- \<open>does not solve it directly!\<close>
+apply (rule rules)+  \<comment> \<open>does not solve it directly!\<close>
 back
 back
 done
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Propositional_Cla.thy
--- a/src/FOL/ex/Propositional_Cla.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Propositional_Cla.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -9,7 +9,7 @@
 imports FOL
 begin
 
-text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>commutative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
 
 lemma "P \<and> Q \<longrightarrow> Q \<and> P"
   by (tactic "IntPr.fast_tac @{context} 1")
@@ -18,7 +18,7 @@
   by fast
 
 
-text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>associative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
 lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
   by fast
 
@@ -26,7 +26,7 @@
   by fast
 
 
-text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>distributive laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
 lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   by fast
 
@@ -60,16 +60,16 @@
 
 text \<open>Propositions-as-types\<close>
 
--- \<open>The combinator K\<close>
+\<comment> \<open>The combinator K\<close>
 lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
   by fast
 
--- \<open>The combinator S\<close>
+\<comment> \<open>The combinator S\<close>
 lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
   by fast
 
 
--- \<open>Converse is classical\<close>
+\<comment> \<open>Converse is classical\<close>
 lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
   by fast
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Propositional_Int.thy
--- a/src/FOL/ex/Propositional_Int.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Propositional_Int.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -9,7 +9,7 @@
 imports IFOL
 begin
 
-text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>commutative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
 
 lemma "P \<and> Q \<longrightarrow> Q \<and> P"
   by (tactic "IntPr.fast_tac @{context} 1")
@@ -18,7 +18,7 @@
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
-text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>associative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
 lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
@@ -26,7 +26,7 @@
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
-text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>distributive laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
 lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
@@ -60,16 +60,16 @@
 
 text \<open>Propositions-as-types\<close>
 
--- \<open>The combinator K\<close>
+\<comment> \<open>The combinator K\<close>
 lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
--- \<open>The combinator S\<close>
+\<comment> \<open>The combinator S\<close>
 lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
--- \<open>Converse is classical\<close>
+\<comment> \<open>Converse is classical\<close>
 lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Quantifiers_Cla.thy
--- a/src/FOL/ex/Quantifiers_Cla.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Quantifiers_Cla.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -33,14 +33,14 @@
 lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
   by fast
 
--- \<open>Converse is false.\<close>
+\<comment> \<open>Converse is false.\<close>
 lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
   by fast
 
 
 text \<open>Basic test of quantifier reasoning.\<close>
 
--- \<open>TRUE\<close>
+\<comment> \<open>TRUE\<close>
 lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
   by fast
 
@@ -72,7 +72,7 @@
 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
-text \<open>An example of why @{text exI} should be delayed as long as possible.\<close>
+text \<open>An example of why \<open>exI\<close> should be delayed as long as possible.\<close>
 lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOL/ex/Quantifiers_Int.thy
--- a/src/FOL/ex/Quantifiers_Int.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Quantifiers_Int.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -16,7 +16,7 @@
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
--- \<open>Converse is false\<close>
+\<comment> \<open>Converse is false\<close>
 lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
@@ -33,14 +33,14 @@
 lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
--- \<open>Converse is false\<close>
+\<comment> \<open>Converse is false\<close>
 lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Basic test of quantifier reasoning\<close>
 
--- \<open>TRUE\<close>
+\<comment> \<open>TRUE\<close>
 lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
@@ -72,7 +72,7 @@
 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
--- \<open>An example of why exI should be delayed as long as possible\<close>
+\<comment> \<open>An example of why exI should be delayed as long as possible\<close>
 lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
@@ -85,7 +85,7 @@
 
 text \<open>Some slow ones\<close>
 
--- \<open>Principia Mathematica *11.53\<close>
+\<comment> \<open>Principia Mathematica *11.53\<close>
 lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOLP/ex/Intro.thy
--- a/src/FOLP/ex/Intro.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOLP/ex/Intro.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -41,7 +41,7 @@
 done
 
 
-subsubsection \<open>Demonstration of @{text "fast"}\<close>
+subsubsection \<open>Demonstration of \<open>fast\<close>\<close>
 
 schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
         -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
diff -r 9de1eb745aeb -r 5d208fd2507d src/FOLP/ex/Intuitionistic.thy
--- a/src/FOLP/ex/Intuitionistic.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOLP/ex/Intuitionistic.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -138,7 +138,7 @@
 
 text "Problem ~~17"
 schematic_goal "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)  -- slow
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)  \<comment> slow
 
 
 subsection \<open>Examples with quantifiers\<close>
@@ -261,7 +261,7 @@
         (ALL x. S(x) & R(x) --> L(x)) &  
         (ALL x. M(x) --> R(x))   
     --> (ALL x. P(x) & M(x) --> L(x))"
-  by (tactic "IntPr.best_tac @{context} 1") -- slow
+  by (tactic "IntPr.best_tac @{context} 1") \<comment> slow
 
 text "Problem 39"
 schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
@@ -270,7 +270,7 @@
 text "Problem 40.  AMENDED"
 schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
               ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-  by (tactic "IntPr.best_tac @{context} 1") -- slow
+  by (tactic "IntPr.best_tac @{context} 1") \<comment> slow
 
 text "Problem 44"
 schematic_goal "?p : (ALL x. f(x) -->                                    
@@ -287,7 +287,7 @@
 schematic_goal
     "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
      (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-  by (tactic "IntPr.best_tac @{context} 1") -- \<open>60 seconds\<close>
+  by (tactic "IntPr.best_tac @{context} 1") \<comment> \<open>60 seconds\<close>
 
 text "Problem 56"
 schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
diff -r 9de1eb745aeb -r 5d208fd2507d src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/Tools/Adhoc_Overloading.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -2,7 +2,7 @@
    Author: Christian Sternagel, University of Innsbruck
 *)
 
-section {* Adhoc overloading of constants based on their types *}
+section \<open>Adhoc overloading of constants based on their types\<close>
 
 theory Adhoc_Overloading
 imports Pure
diff -r 9de1eb745aeb -r 5d208fd2507d src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/Tools/Code_Generator.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -2,7 +2,7 @@
     Author:  Florian Haftmann, TU Muenchen
 *)
 
-section {* Loading the code generator and related modules *}
+section \<open>Loading the code generator and related modules\<close>
 
 theory Code_Generator
 imports Pure
diff -r 9de1eb745aeb -r 5d208fd2507d src/Tools/Spec_Check/Examples.thy
--- a/src/Tools/Spec_Check/Examples.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/Tools/Spec_Check/Examples.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -2,82 +2,82 @@
 imports Spec_Check
 begin
 
-section {* List examples *}
+section \<open>List examples\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL xs. rev xs = xs";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL xs. rev (rev xs) = xs";
-*}
+\<close>
 
 
-section {* AList Specification *}
+section \<open>AList Specification\<close>
 
-ML_command {*
+ML_command \<open>
 (* map_entry applies the function to the element *)
 check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 (* update always results in an entry *)
 check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 (* update always writes the value *)
 check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 (* default always results in an entry *)
 check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 (* delete always removes the entry *)
 check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 (* default writes the entry iff it didn't exist *)
 check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
-*}
+\<close>
 
-section {* Examples on Types and Terms *}
+section \<open>Examples on Types and Terms\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
-*}
+\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
-*}
+\<close>
 
 
-text {* One would think this holds: *}
+text \<open>One would think this holds:\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
-*}
+\<close>
 
-text {* But it only holds with this precondition: *}
+text \<open>But it only holds with this precondition:\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
-*}
+\<close>
 
-section {* Some surprises *}
+section \<open>Some surprises\<close>
 
-ML_command {*
+ML_command \<open>
 check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
-*}
+\<close>
 
 
-ML_command {*
+ML_command \<open>
 val thy = @{theory};
 check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
-*}
+\<close>
 
 end