--- 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]])
--- 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
--- 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>
--- 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} *)
--- 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)
--- 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'"
--- 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
--- 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])
--- 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)
--- 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
--- 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"
--- 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>
--- 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
--- 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
--- 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))"
--- 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
--- 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>
--- 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
--- 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
--- 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")
--- 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
--- 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")
--- 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))"
--- 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)))"
--- 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
--- 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
--- 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