--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Sat Dec 26 15:59:27 2015 +0100
@@ -30,7 +30,7 @@
text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
rewrite systems (i.e., sets of rules), the set of variables makes
-sense. Thus we introduce an unspecified constant @{text vars}.\<close>
+sense. Thus we introduce an unspecified constant \<open>vars\<close>.\<close>
consts vars :: "'a \<Rightarrow> 'b set"
@@ -69,7 +69,7 @@
text \<open>As stated earlier, the overloaded constant is only used for
input and output. Internally, always a variant is used, as can be
-observed by the configuration option @{text show_variants}.\<close>
+observed by the configuration option \<open>show_variants\<close>.\<close>
adhoc_overloading
vars term_vars
@@ -173,7 +173,7 @@
section \<open>Permutation Types\<close>
text \<open>We want to be able to apply permutations to arbitrary types. To
-this end we introduce a constant @{text PERMUTE} together with
+this end we introduce a constant \<open>PERMUTE\<close> together with
convenient infix syntax.\<close>
consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
--- a/src/HOL/ex/Antiquote.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Antiquote.thy Sat Dec 26 15:59:27 2015 +0100
@@ -31,9 +31,9 @@
term "EXPR (a + b + c + VAR x + VAR y + 1)"
term "EXPR (VAR (f w) + VAR x)"
-term "Expr (\<lambda>env. env x)" -- \<open>improper\<close>
+term "Expr (\<lambda>env. env x)" \<comment> \<open>improper\<close>
term "Expr (\<lambda>env. f env)"
-term "Expr (\<lambda>env. f env + env x)" -- \<open>improper\<close>
+term "Expr (\<lambda>env. f env + env x)" \<comment> \<open>improper\<close>
term "Expr (\<lambda>env. f env y z)"
term "Expr (\<lambda>env. f env + g y env)"
term "Expr (\<lambda>env. f env + g env y + h a env z)"
--- a/src/HOL/ex/Arith_Examples.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Arith_Examples.thy Sat Dec 26 15:59:27 2015 +0100
@@ -9,18 +9,18 @@
begin
text \<open>
- The @{text arith} method is used frequently throughout the Isabelle
+ The \<open>arith\<close> method is used frequently throughout the Isabelle
distribution. This file merely contains some additional tests and special
corner cases. Some rather technical remarks:
@{ML Lin_Arith.simple_tac} is a very basic version of the tactic. It performs no
meta-to-object-logic conversion, and only some splitting of operators.
@{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
- splitting of operators, and NNF normalization of the goal. The @{text arith}
- method combines them both, and tries other methods (e.g.~@{text presburger})
+ splitting of operators, and NNF normalization of the goal. The \<open>arith\<close>
+ method combines them both, and tries other methods (e.g.~\<open>presburger\<close>)
as well. This is the one that you should use in your proofs!
- An @{text arith}-based simproc is available as well (see @{ML
+ An \<open>arith\<close>-based simproc is available as well (see @{ML
Lin_Arith.simproc}), which---for performance
reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
at the moment (namely inequalities only). (On the other hand, it
--- a/src/HOL/ex/CTL.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/CTL.thy Sat Dec 26 15:59:27 2015 +0100
@@ -35,26 +35,25 @@
text \<open>
\smallskip The CTL path operators are more interesting; they are
- based on an arbitrary, but fixed model @{text \<M>}, which is simply
+ based on an arbitrary, but fixed model \<open>\<M>\<close>, which is simply
a transition relation over states @{typ "'a"}.
\<close>
axiomatization \<M> :: "('a \<times> 'a) set"
text \<open>
- The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
- as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
- defined as derived ones. The formula @{text "\<EX> p"} holds in a
+ The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken
+ as primitives, while \<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are
+ defined as derived ones. The formula \<open>\<EX> p\<close> holds in a
state @{term s}, iff there is a successor state @{term s'} (with
respect to the model @{term \<M>}), such that @{term p} holds in
- @{term s'}. The formula @{text "\<EF> p"} holds in a state @{term
- s}, iff there is a path in @{text \<M>}, starting from @{term s},
+ @{term s'}. The formula \<open>\<EF> p\<close> holds in a state @{term
+ s}, iff there is a path in \<open>\<M>\<close>, starting from @{term s},
such that there exists a state @{term s'} on the path, such that
- @{term p} holds in @{term s'}. The formula @{text "\<EG> p"} holds
+ @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close> holds
in a state @{term s}, iff there is a path, starting from @{term s},
such that for all states @{term s'} on the path, @{term p} holds in
- @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text
- "\<EG> p"} may be expressed using least and greatest fixed points
+ @{term s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using least and greatest fixed points
@{cite "McMillan-PhDThesis"}.
\<close>
@@ -66,9 +65,8 @@
EG ("\<EG> _" [80] 90) where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
text \<open>
- @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
- dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
- "\<EG>"}.
+ \<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined
+ dually in terms of \<open>\<EX>\<close>, \<open>\<EF>\<close> and \<open>\<EG>\<close>.
\<close>
definition
@@ -160,8 +158,8 @@
text \<open>
This fact may be split up into two inequalities (merely using
- transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
- @{text "\<le>"} in Isabelle/HOL).
+ transitivity of \<open>\<subseteq>\<close>, which is an instance of the overloaded
+ \<open>\<le>\<close> in Isabelle/HOL).
\<close>
lemma AG_fp_1: "\<AG> p \<subseteq> p"
@@ -193,7 +191,7 @@
text \<open>
With the most basic facts available, we are now able to establish a
few more interesting results, leading to the \emph{tree induction}
- principle for @{text AG} (see below). We will use some elementary
+ principle for \<open>AG\<close> (see below). We will use some elementary
monotonicity and distributivity rules.
\<close>
@@ -204,7 +202,7 @@
text \<open>
The formula @{term "AG p"} implies @{term "AX p"} (we use
- substitution of @{text "\<subseteq>"} with monotonicity).
+ substitution of \<open>\<subseteq>\<close> with monotonicity).
\<close>
lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
@@ -215,7 +213,7 @@
qed
text \<open>
- Furthermore we show idempotency of the @{text "\<AG>"} operator.
+ Furthermore we show idempotency of the \<open>\<AG>\<close> operator.
The proof is a good example of how accumulated facts may get
used to feed a single rule step.
\<close>
@@ -233,8 +231,7 @@
qed
text \<open>
- \smallskip We now give an alternative characterization of the @{text
- "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
+ \smallskip We now give an alternative characterization of the \<open>\<AG>\<close> operator, which describes the \<open>\<AG>\<close> operator in
an ``operational'' way by tree induction: In a state holds @{term
"AG p"} iff in that state holds @{term p}, and in all reachable
states @{term s} follows from the fact that @{term p} holds in
@@ -289,7 +286,7 @@
text \<open>
Further interesting properties of CTL expressions may be
demonstrated with the help of tree induction; here we show that
- @{text \<AX>} and @{text \<AG>} commute.
+ \<open>\<AX>\<close> and \<open>\<AG>\<close> commute.
\<close>
theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
--- a/src/HOL/ex/Cartouche_Examples.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Sat Dec 26 15:59:27 2015 +0100
@@ -15,7 +15,7 @@
text \<open>Text cartouches may be used in the outer syntax category "text",
as alternative to the traditional "verbatim" tokens. An example is
- this text block.\<close> -- \<open>The same works for small side-comments.\<close>
+ this text block.\<close> \<comment> \<open>The same works for small side-comments.\<close>
notepad
begin
@@ -33,7 +33,7 @@
[OF \<open>x = y\<close>]}.\<close>
have "x = y"
- by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>) -- \<open>more cartouches involving ML\<close>
+ by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>) \<comment> \<open>more cartouches involving ML\<close>
end
@@ -134,14 +134,14 @@
subsubsection \<open>Further nesting: antiquotations\<close>
-setup -- "ML antiquotation"
+setup \<comment> "ML antiquotation"
\<open>
ML_Antiquotation.inline @{binding term_cartouche}
(Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
(fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
\<close>
-setup -- "document antiquotation"
+setup \<comment> "document antiquotation"
\<open>
Thy_Output.antiquotation @{binding ML_cartouche}
(Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
--- a/src/HOL/ex/Classical.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Classical.thy Sat Dec 26 15:59:27 2015 +0100
@@ -11,9 +11,8 @@
text\<open>The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.\<close>
-text\<open>Taken from @{text "FOL/Classical.thy"}. When porting examples from
-first-order logic, beware of the precedence of @{text "="} versus @{text
-"\<leftrightarrow>"}.\<close>
+text\<open>Taken from \<open>FOL/Classical.thy\<close>. When porting examples from
+first-order logic, beware of the precedence of \<open>=\<close> versus \<open>\<leftrightarrow>\<close>.\<close>
lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
by blast
@@ -430,7 +429,7 @@
(\<forall>x. \<exists>y. R(x,y)) -->
~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
- --\<open>In contrast, @{text meson} is SLOW: 7.6s on griffon\<close>
+ \<comment>\<open>In contrast, \<open>meson\<close> is SLOW: 7.6s on griffon\<close>
subsubsection\<open>Pelletier's examples\<close>
@@ -645,7 +644,7 @@
(\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &
((\<exists>x y. Q x y) --> (\<forall>x. R x x))
--> (\<forall>x. \<exists>y. R x y)"
-by blast --\<open>causes unification tracing messages\<close>
+by blast \<comment>\<open>causes unification tracing messages\<close>
text\<open>Problem 38\<close> text\<open>Quite hard: 422 Horn clauses!!\<close>
@@ -724,7 +723,7 @@
(\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
\<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
- --\<open>Nearly twice as fast as @{text meson},
+ \<comment>\<open>Nearly twice as fast as \<open>meson\<close>,
which performs iterative deepening rather than best-first search\<close>
text\<open>The Los problem. Circulated by John Harrison\<close>
@@ -756,7 +755,7 @@
text\<open>Problem 55\<close>
text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
- @{text meson} cannot report who killed Agatha.\<close>
+ \<open>meson\<close> cannot report who killed Agatha.\<close>
lemma "lives agatha & lives butler & lives charles &
(killed agatha agatha | killed butler agatha | killed charles agatha) &
(\<forall>x y. killed x y --> hates x y & ~richer x y) &
@@ -802,13 +801,13 @@
shows True
proof -
from a b d have "\<forall>x. T(i x x)" by blast
- from a b c d have "\<forall>x. T(i x (n(n x)))" --\<open>Problem 66\<close>
+ from a b c d have "\<forall>x. T(i x (n(n x)))" \<comment>\<open>Problem 66\<close>
by metis
- from a b c d have "\<forall>x. T(i (n(n x)) x)" --\<open>Problem 67\<close>
+ from a b c d have "\<forall>x. T(i (n(n x)) x)" \<comment>\<open>Problem 67\<close>
by meson
- --\<open>4.9s on griffon. 51061 inferences, depth 21\<close>
+ \<comment>\<open>4.9s on griffon. 51061 inferences, depth 21\<close>
from a b c' d have "\<forall>x. T(i x (n(n x)))"
- --\<open>Problem 68: not proved. Listed as satisfiable in TPTP (LCL078-1)\<close>
+ \<comment>\<open>Problem 68: not proved. Listed as satisfiable in TPTP (LCL078-1)\<close>
oops
text\<open>Problem 71, as found in TPTP (SYN007+1.005)\<close>
--- a/src/HOL/ex/Dedekind_Real.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Sat Dec 26 15:59:27 2015 +0100
@@ -13,7 +13,7 @@
section \<open>Positive real numbers\<close>
-text\<open>Could be generalized and moved to @{text Groups}\<close>
+text\<open>Could be generalized and moved to \<open>Groups\<close>\<close>
lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
by (rule_tac x="b-a" in exI, simp)
@@ -250,7 +250,7 @@
done
text\<open>Part 2 of Dedekind sections definition. A structured version of
-this proof is @{text preal_not_mem_mult_set_Ex} below.\<close>
+this proof is \<open>preal_not_mem_mult_set_Ex\<close> below.\<close>
lemma preal_not_mem_add_set_Ex:
"[|cut A; cut B|] ==> \<exists>q>0. q \<notin> add_set A B"
apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto)
@@ -881,7 +881,7 @@
done
-text\<open>Theorems needing @{text Gleason9_34}\<close>
+text\<open>Theorems needing \<open>Gleason9_34\<close>\<close>
lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
proof
@@ -1443,7 +1443,7 @@
qed
-subsection\<open>The @{text "\<le>"} Ordering\<close>
+subsection\<open>The \<open>\<le>\<close> Ordering\<close>
lemma real_le_refl: "w \<le> (w::real)"
by (cases w, force simp add: real_le_def)
@@ -1544,7 +1544,7 @@
apply (simp add: linorder_not_le [where 'a = real, symmetric]
linorder_not_le [where 'a = preal]
real_zero_def real_le real_mult)
- --\<open>Reduce to the (simpler) @{text "\<le>"} relation\<close>
+ \<comment>\<open>Reduce to the (simpler) \<open>\<le>\<close> relation\<close>
apply (auto dest!: less_add_left_Ex
simp add: algebra_simps preal_self_less_add_left)
done
@@ -1670,11 +1670,11 @@
text \<open>
Supremum property for the set of positive reals
- Let @{text "P"} be a non-empty set of positive reals, with an upper
- bound @{text "y"}. Then @{text "P"} has a least upper bound
- (written @{text "S"}).
+ Let \<open>P\<close> be a non-empty set of positive reals, with an upper
+ bound \<open>y\<close>. Then \<open>P\<close> has a least upper bound
+ (written \<open>S\<close>).
- FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}?
+ FIXME: Can the premise be weakened to \<open>\<forall>x \<in> P. x\<le> y\<close>?
\<close>
lemma posreal_complete:
@@ -1908,8 +1908,8 @@
qed
text \<open>
- There must be other proofs, e.g. @{text Suc} of the largest
- integer in the cut representing @{text "x"}.
+ There must be other proofs, e.g. \<open>Suc\<close> of the largest
+ integer in the cut representing \<open>x\<close>.
\<close>
lemma reals_Archimedean2: "\<exists>n. (x::real) < of_nat (n::nat)"
--- a/src/HOL/ex/Execute_Choice.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Execute_Choice.thy Sat Dec 26 15:59:27 2015 +0100
@@ -57,7 +57,7 @@
unfolding valuesum_def by transfer (simp add: setsum_diff)
text \<open>
- Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
+ Given \<open>valuesum_rec\<close> as initial description, we stepwise refine it to something executable;
first, we formally insert the constructor @{term Mapping} and split the one equation into two,
where the second one provides the necessary context:
\<close>
@@ -72,7 +72,7 @@
As a side effect the precondition disappears (but note this has nothing to do with choice!).
The first equation deals with the uncritical empty case and can already be used for code generation.
- Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
+ Using \<open>valuesum_choice\<close>, we are able to prove an executable version of @{term valuesum}:
\<close>
lemma valuesum_rec_exec [code]:
--- a/src/HOL/ex/FinFunPred.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/FinFunPred.thy Sat Dec 26 15:59:27 2015 +0100
@@ -126,7 +126,7 @@
by(simp add: le_finfun_def)
text \<open>Bounded quantification.
- Warning: @{text "finfun_Ball"} and @{text "finfun_Ex"} may raise an exception, they should not be used for quickcheck
+ Warning: \<open>finfun_Ball\<close> and \<open>finfun_Ex\<close> may raise an exception, they should not be used for quickcheck
\<close>
definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^sub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -237,7 +237,7 @@
by(simp)
text \<open>
- Do not declare the following two theorems as @{text "[code_unfold]"},
+ Do not declare the following two theorems as \<open>[code_unfold]\<close>,
because this causes quickcheck to fail frequently when bounded quantification is used which raises an exception.
For code generation, the same problems occur, but then, no randomly generated FinFun is usually around.
\<close>
--- a/src/HOL/ex/Fundefs.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Fundefs.thy Sat Dec 26 15:59:27 2015 +0100
@@ -39,7 +39,7 @@
| "add (Suc x) y = Suc (add x y)"
thm add.simps
-thm add.induct -- \<open>Note the curried induction predicate\<close>
+thm add.induct \<comment> \<open>Note the curried induction predicate\<close>
subsection \<open>Nested recursion\<close>
@@ -50,7 +50,7 @@
| "nz (Suc x) = nz (nz x)"
by pat_completeness auto
-lemma nz_is_zero: -- \<open>A lemma we need to prove termination\<close>
+lemma nz_is_zero: \<comment> \<open>A lemma we need to prove termination\<close>
assumes trm: "nz_dom x"
shows "nz x = 0"
using trm
@@ -137,7 +137,7 @@
where
"ev (2 * n) = True"
| "ev (2 * n + 1) = False"
-proof - -- \<open>completeness is more difficult here \dots\<close>
+proof - \<comment> \<open>completeness is more difficult here \dots\<close>
fix P :: bool
and x :: nat
assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
@@ -154,7 +154,7 @@
with divmod have "x = 2 * (x div 2) + 1" by simp
with c2 show "P" .
qed
-qed presburger+ -- \<open>solve compatibility with presburger\<close>
+qed presburger+ \<comment> \<open>solve compatibility with presburger\<close>
termination by lexicographic_order
thm ev.simps
@@ -213,7 +213,7 @@
thm my_monoid.foldL.simps
thm my_monoid.foldR_foldL
-subsection \<open>@{text fun_cases}\<close>
+subsection \<open>\<open>fun_cases\<close>\<close>
subsubsection \<open>Predecessor\<close>
@@ -265,7 +265,7 @@
thm xor.elims
-text \<open>@{text fun_cases} does not only recognise function equations, but also works with
+text \<open>\<open>fun_cases\<close> does not only recognise function equations, but also works with
functions that return a boolean, e.g.:\<close>
fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b"
--- a/src/HOL/ex/HarmonicSeries.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy Sat Dec 26 15:59:27 2015 +0100
@@ -138,7 +138,7 @@
have ant: "0 < Suc M" by fact
{
have suc: "?LHS (Suc M) = ?RHS (Suc M)"
- proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS"
+ proof cases \<comment> "show that LHS = c and RHS = c, and thus LHS = RHS"
assume mz: "M=0"
{
then have
@@ -274,8 +274,8 @@
theorem DivergenceOfHarmonicSeries:
shows "\<not>summable (\<lambda>n. 1/real (Suc n))"
(is "\<not>summable ?f")
-proof -- "by contradiction"
- let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series"
+proof \<comment> "by contradiction"
+ let ?s = "suminf ?f" \<comment> "let ?s equal the sum of the harmonic series"
assume sf: "summable ?f"
then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
then have ngt: "1 + real n/2 > ?s" by linarith
--- a/src/HOL/ex/LocaleTest2.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Sat Dec 26 15:59:27 2015 +0100
@@ -466,16 +466,16 @@
qed
qed
-subsubsection \<open>Total order @{text "<="} on @{typ int}\<close>
+subsubsection \<open>Total order \<open><=\<close> on @{typ int}\<close>
interpretation int: dpo "op <= :: [int, int] => bool"
rewrites "(dpo.less (op <=) (x::int) y) = (x < y)"
- txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
+ txt \<open>We give interpretation for less, but not \<open>is_inf\<close> and \<open>is_sub\<close>.\<close>
proof -
show "dpo (op <= :: [int, int] => bool)"
proof qed auto
then interpret int: dpo "op <= :: [int, int] => bool" .
- txt \<open>Gives interpreted version of @{text less_def} (without condition).\<close>
+ txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
show "(dpo.less (op <=) (x::int) y) = (x < y)"
by (unfold int.less_def) auto
qed
@@ -522,16 +522,16 @@
thm int.less_total text \<open>from dlo\<close>
-subsubsection \<open>Total order @{text "<="} on @{typ nat}\<close>
+subsubsection \<open>Total order \<open><=\<close> on @{typ nat}\<close>
interpretation nat: dpo "op <= :: [nat, nat] => bool"
rewrites "dpo.less (op <=) (x::nat) y = (x < y)"
- txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
+ txt \<open>We give interpretation for less, but not \<open>is_inf\<close> and \<open>is_sub\<close>.\<close>
proof -
show "dpo (op <= :: [nat, nat] => bool)"
proof qed auto
then interpret nat: dpo "op <= :: [nat, nat] => bool" .
- txt \<open>Gives interpreted version of @{text less_def} (without condition).\<close>
+ txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
show "dpo.less (op <=) (x::nat) y = (x < y)"
apply (unfold nat.less_def)
apply auto
@@ -573,16 +573,16 @@
thm nat.less_total text \<open>from ldo\<close>
-subsubsection \<open>Lattice @{text "dvd"} on @{typ nat}\<close>
+subsubsection \<open>Lattice \<open>dvd\<close> on @{typ nat}\<close>
interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
rewrites "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
- txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
+ txt \<open>We give interpretation for less, but not \<open>is_inf\<close> and \<open>is_sub\<close>.\<close>
proof -
show "dpo (op dvd :: [nat, nat] => bool)"
proof qed (auto simp: dvd_def)
then interpret nat_dvd: dpo "op dvd :: [nat, nat] => bool" .
- txt \<open>Gives interpreted version of @{text less_def} (without condition).\<close>
+ txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
apply (unfold nat_dvd.less_def)
apply auto
@@ -626,7 +626,7 @@
apply (rule nat_dvd.meet_left) done
-subsection \<open>Group example with defined operations @{text inv} and @{text unit}\<close>
+subsection \<open>Group example with defined operations \<open>inv\<close> and \<open>unit\<close>\<close>
subsubsection \<open>Locale declarations and lemmas\<close>
--- a/src/HOL/ex/Meson_Test.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Meson_Test.thy Sat Dec 26 15:59:27 2015 +0100
@@ -71,7 +71,7 @@
\<close>
oops
-lemma problem_43: -- "NOW PROVED AUTOMATICALLY!!" (*16 Horn clauses*)
+lemma problem_43: \<comment> "NOW PROVED AUTOMATICALLY!!" (*16 Horn clauses*)
"(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool))) --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
apply (rule ccontr)
ML_prf \<open>
--- a/src/HOL/ex/NatSum.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/NatSum.thy Sat Dec 26 15:59:27 2015 +0100
@@ -15,10 +15,10 @@
lemmas [simp] =
ring_distribs
- diff_mult_distrib diff_mult_distrib2 --\<open>for type nat\<close>
+ diff_mult_distrib diff_mult_distrib2 \<comment>\<open>for type nat\<close>
text \<open>
- \medskip The sum of the first @{text n} odd numbers equals @{text n}
+ \medskip The sum of the first \<open>n\<close> odd numbers equals \<open>n\<close>
squared.
\<close>
@@ -27,7 +27,7 @@
text \<open>
- \medskip The sum of the first @{text n} odd squares.
+ \medskip The sum of the first \<open>n\<close> odd squares.
\<close>
lemma sum_of_odd_squares:
@@ -36,7 +36,7 @@
text \<open>
- \medskip The sum of the first @{text n} odd cubes
+ \medskip The sum of the first \<open>n\<close> odd cubes
\<close>
lemma sum_of_odd_cubes:
@@ -45,8 +45,8 @@
by (induct n) auto
text \<open>
- \medskip The sum of the first @{text n} positive integers equals
- @{text "n (n + 1) / 2"}.\<close>
+ \medskip The sum of the first \<open>n\<close> positive integers equals
+ \<open>n (n + 1) / 2\<close>.\<close>
lemma sum_of_naturals:
"2 * (\<Sum>i=0..n. i) = n * Suc n"
@@ -86,7 +86,7 @@
n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
apply (induct n)
apply simp_all
- apply (case_tac n) -- \<open>eliminates the subtraction\<close>
+ apply (case_tac n) \<comment> \<open>eliminates the subtraction\<close>
apply (simp_all (no_asm_simp))
done
@@ -108,7 +108,7 @@
text \<open>
- \medskip Sums of geometric series: @{text 2}, @{text 3} and the
+ \medskip Sums of geometric series: \<open>2\<close>, \<open>3\<close> and the
general case.
\<close>
--- a/src/HOL/ex/PER.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/PER.thy Sat Dec 26 15:59:27 2015 +0100
@@ -11,8 +11,8 @@
text \<open>
Higher-order quotients are defined over partial equivalence
relations (PERs) instead of total ones. We provide axiomatic type
- classes @{text "equiv < partial_equiv"} and a type constructor
- @{text "'a quot"} with basic operations. This development is based
+ classes \<open>equiv < partial_equiv\<close> and a type constructor
+ \<open>'a quot\<close> with basic operations. This development is based
on:
Oscar Slotosch: \emph{Higher Order Quotients and their
@@ -25,9 +25,9 @@
subsection \<open>Partial equivalence\<close>
text \<open>
- Type class @{text partial_equiv} models partial equivalence
- relations (PERs) using the polymorphic @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
- bool"} relation, which is required to be symmetric and transitive,
+ Type class \<open>partial_equiv\<close> models partial equivalence
+ relations (PERs) using the polymorphic \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
+ bool\<close> relation, which is required to be symmetric and transitive,
but not necessarily reflexive.
\<close>
@@ -64,7 +64,7 @@
subsection \<open>Equivalence on function spaces\<close>
text \<open>
- The @{text \<sim>} relation is lifted to function spaces. It is
+ The \<open>\<sim>\<close> relation is lifted to function spaces. It is
important to note that this is \emph{not} the direct product, but a
structural one corresponding to the congruence property.
\<close>
@@ -117,8 +117,8 @@
text \<open>
The class of total equivalence relations on top of PERs. It
- coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
- :: 'a \<Rightarrow> 'a \<Rightarrow> bool"} is required to be reflexive, transitive and
+ coincides with the standard notion of equivalence, i.e.\ \<open>\<sim>
+ :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close> is required to be reflexive, transitive and
symmetric.
\<close>
@@ -148,7 +148,7 @@
subsection \<open>Quotient types\<close>
text \<open>
- The quotient type @{text "'a quot"} consists of all
+ The quotient type \<open>'a quot\<close> consists of all
\emph{equivalence classes} over elements of the base type @{typ 'a}.
\<close>
--- a/src/HOL/ex/Parallel_Example.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Parallel_Example.thy Sat Dec 26 15:59:27 2015 +0100
@@ -34,7 +34,7 @@
| p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
by pat_completeness auto
-termination -- \<open>tuning of this proof is left as an exercise to the reader\<close>
+termination \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
apply (relation "measure (length \<circ> snd)")
apply rule
apply (auto simp add: length_dropWhile_le)
@@ -67,7 +67,7 @@
else [])"
by pat_completeness auto
-termination factorise_from -- \<open>tuning of this proof is left as an exercise to the reader\<close>
+termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
term measure
apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
apply (auto simp add: prod_eq_iff)
--- a/src/HOL/ex/Primrec.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Primrec.thy Sat Dec 26 15:59:27 2015 +0100
@@ -43,14 +43,14 @@
by (induct i j rule: ack.induct) simp_all
-text \<open>PROPERTY A 5, monotonicity for @{text "<"}\<close>
+text \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close>
lemma ack_less_mono2: "j < k ==> ack i j < ack i k"
using lift_Suc_mono_less[where f = "ack i"]
by (metis ack_less_ack_Suc2)
-text \<open>PROPERTY A 5', monotonicity for @{text \<le>}\<close>
+text \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close>
lemma ack_le_mono2: "j \<le> k ==> ack i j \<le> ack i k"
apply (simp add: order_le_less)
@@ -91,14 +91,14 @@
by (induct j) simp_all
-text \<open>PROPERTY A 9. The unary @{text 1} and @{text 2} in @{term
+text \<open>PROPERTY A 9. The unary \<open>1\<close> and \<open>2\<close> in @{term
ack} is essential for the rewriting.\<close>
lemma ack_2 [simp]: "ack (Suc (Suc 0)) j = 2 * j + 3"
by (induct j) simp_all
-text \<open>PROPERTY A 7, monotonicity for @{text "<"} [not clear why
+text \<open>PROPERTY A 7, monotonicity for \<open><\<close> [not clear why
@{thm [source] ack_1} is now needed first!]\<close>
lemma ack_less_mono1_aux: "ack i k < ack (Suc (i +i')) k"
@@ -118,7 +118,7 @@
done
-text \<open>PROPERTY A 7', monotonicity for @{text "\<le>"}\<close>
+text \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close>
lemma ack_le_mono1: "i \<le> j ==> ack i k \<le> ack j k"
apply (simp add: order_le_less)
@@ -153,8 +153,7 @@
text \<open>PROPERTY A 12. Article uses existential quantifier but the ALF proof
- used @{text "k + 4"}. Quantified version must be nested @{text
- "\<exists>k'. \<forall>i j. ..."}\<close>
+ used \<open>k + 4\<close>. Quantified version must be nested \<open>\<exists>k'. \<forall>i j. ...\<close>\<close>
lemma ack_add_bound2: "i < ack k j ==> i + j < ack (4 + k) j"
apply (rule less_trans [of _ "ack k j + ack 0 j"])
@@ -192,7 +191,7 @@
(case l of
[] => 0
| x # l' => rec_nat (f l') (\<lambda>y r. g (r # y # l')) x)"
- -- \<open>Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}!\<close>
+ \<comment> \<open>Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}!\<close>
inductive PRIMREC :: "(nat list => nat) => bool" where
SC: "PRIMREC SC" |
@@ -273,7 +272,7 @@
apply (case_tac l)
apply simp_all
apply (blast intro: less_trans)
-apply (erule ssubst) -- \<open>get rid of the needless assumption\<close>
+apply (erule ssubst) \<comment> \<open>get rid of the needless assumption\<close>
apply (induct_tac a)
apply simp_all
txt \<open>base case\<close>
--- a/src/HOL/ex/Records.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Records.thy Sat Dec 26 15:59:27 2015 +0100
@@ -75,19 +75,19 @@
text \<open>\medskip Equality of records.\<close>
lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
- -- "introduction of concrete record equality"
+ \<comment> "introduction of concrete record equality"
by simp
lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
- -- "elimination of concrete record equality"
+ \<comment> "elimination of concrete record equality"
by simp
lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
- -- "introduction of abstract record equality"
+ \<comment> "introduction of abstract record equality"
by simp
lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
- -- "elimination of abstract record equality (manual proof)"
+ \<comment> "elimination of abstract record equality (manual proof)"
proof -
assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
then have "xpos ?lhs = xpos ?rhs" by simp
@@ -149,7 +149,7 @@
where "foo5 = getX (| xpos = 1, ypos = 0 |)"
-text \<open>\medskip Manipulating the ``@{text "..."}'' (more) part.\<close>
+text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close>
definition incX :: "'a point_scheme => 'a point_scheme"
where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
@@ -188,7 +188,7 @@
text \<open>
- Functions on @{text point} schemes work for @{text cpoints} as well.
+ Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.
\<close>
definition foo10 :: nat
--- a/src/HOL/ex/Reflection_Examples.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Reflection_Examples.thy Sat Dec 26 15:59:27 2015 +0100
@@ -11,40 +11,40 @@
text \<open>This theory presents two methods: reify and reflection\<close>
text \<open>
-Consider an HOL type @{text \<sigma>}, the structure of which is not recongnisable
+Consider an HOL type \<open>\<sigma>\<close>, the structure of which is not recongnisable
on the theory level. This is the case of @{typ bool}, arithmetical terms such as @{typ int},
-@{typ real} etc \dots In order to implement a simplification on terms of type @{text \<sigma>} we
+@{typ real} etc \dots In order to implement a simplification on terms of type \<open>\<sigma>\<close> we
often need its structure. Traditionnaly such simplifications are written in ML,
proofs are synthesized.
-An other strategy is to declare an HOL datatype @{text \<tau>} and an HOL function (the
-interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
+An other strategy is to declare an HOL datatype \<open>\<tau>\<close> and an HOL function (the
+interpretation) that maps elements of \<open>\<tau>\<close> to elements of \<open>\<sigma>\<close>.
-The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},
-to compute a term @{text s} of type @{text \<tau>}. For this it needs equations for the
+The functionality of \<open>reify\<close> then is, given a term \<open>t\<close> of type \<open>\<sigma>\<close>,
+to compute a term \<open>s\<close> of type \<open>\<tau>\<close>. For this it needs equations for the
interpretation.
-N.B: All the interpretations supported by @{text reify} must have the type
-@{text "'a list \<Rightarrow> \<tau> \<Rightarrow> \<sigma>"}. The method @{text reify} can also be told which subterm
-of the current subgoal should be reified. The general call for @{text reify} is
-@{text "reify eqs (t)"}, where @{text eqs} are the defining equations of the interpretation
-and @{text "(t)"} is an optional parameter which specifies the subterm to which reification
-should be applied to. If @{text "(t)"} is abscent, @{text reify} tries to reify the whole
+N.B: All the interpretations supported by \<open>reify\<close> must have the type
+\<open>'a list \<Rightarrow> \<tau> \<Rightarrow> \<sigma>\<close>. The method \<open>reify\<close> can also be told which subterm
+of the current subgoal should be reified. The general call for \<open>reify\<close> is
+\<open>reify eqs (t)\<close>, where \<open>eqs\<close> are the defining equations of the interpretation
+and \<open>(t)\<close> is an optional parameter which specifies the subterm to which reification
+should be applied to. If \<open>(t)\<close> is abscent, \<open>reify\<close> tries to reify the whole
subgoal.
-The method @{text reflection} uses @{text reify} and has a very similar signature:
-@{text "reflection corr_thm eqs (t)"}. Here again @{text eqs} and @{text "(t)"}
-are as described above and @{text corr_thm} is a theorem proving
-@{prop "I vs (f t) = I vs t"}. We assume that @{text I} is the interpretation
-and @{text f} is some useful and executable simplification of type @{text "\<tau> \<Rightarrow> \<tau>"}.
-The method @{text reflection} applies reification and hence the theorem @{prop "t = I xs s"}
-and hence using @{text corr_thm} derives @{prop "t = I xs (f s)"}. It then uses
+The method \<open>reflection\<close> uses \<open>reify\<close> and has a very similar signature:
+\<open>reflection corr_thm eqs (t)\<close>. Here again \<open>eqs\<close> and \<open>(t)\<close>
+are as described above and \<open>corr_thm\<close> is a theorem proving
+@{prop "I vs (f t) = I vs t"}. We assume that \<open>I\<close> is the interpretation
+and \<open>f\<close> is some useful and executable simplification of type \<open>\<tau> \<Rightarrow> \<tau>\<close>.
+The method \<open>reflection\<close> applies reification and hence the theorem @{prop "t = I xs s"}
+and hence using \<open>corr_thm\<close> derives @{prop "t = I xs (f s)"}. It then uses
normalization by equational rewriting to prove @{prop "f s = s'"} which almost finishes
the proof of @{prop "t = t'"} where @{prop "I xs s' = t'"}.
\<close>
text \<open>Example 1 : Propositional formulae and NNF.\<close>
-text \<open>The type @{text fm} represents simple propositional formulae:\<close>
+text \<open>The type \<open>fm\<close> represents simple propositional formulae:\<close>
datatype form = TrueF | FalseF | Less nat nat
| And form form | Or form form | Neg form | ExQ form
@@ -81,8 +81,8 @@
apply (reify Ifm.simps)
oops
-text \<open>Method @{text reify} maps a @{typ bool} to an @{typ fm}. For this it needs the
-semantics of @{text fm}, i.e.\ the rewrite rules in @{text Ifm.simps}.\<close>
+text \<open>Method \<open>reify\<close> maps a @{typ bool} to an @{typ fm}. For this it needs the
+semantics of \<open>fm\<close>, i.e.\ the rewrite rules in \<open>Ifm.simps\<close>.\<close>
text \<open>You can also just pick up a subterm to reify.\<close>
lemma "Q \<longrightarrow> (D \<and> F \<and> ((\<not> D) \<and> (\<not> F)))"
@@ -134,7 +134,7 @@
text \<open>Example 2: Simple arithmetic formulae\<close>
-text \<open>The type @{text num} reflects linear expressions over natural number\<close>
+text \<open>The type \<open>num\<close> reflects linear expressions over natural number\<close>
datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
text \<open>This is just technical to make recursive definitions easier.\<close>
@@ -161,15 +161,15 @@
lemma "4 * (2 * x + (y::nat)) + f a \<noteq> 0"
apply (reify Inum.simps ("4 * (2 * x + (y::nat)) + f a"))
oops
-text \<open>We're in a bad situation! @{text x}, @{text y} and @{text f} have been recongnized
+text \<open>We're in a bad situation! \<open>x\<close>, \<open>y\<close> and \<open>f\<close> have been recongnized
as constants, which is correct but does not correspond to our intuition of the constructor C.
It should encapsulate constants, i.e. numbers, i.e. numerals.\<close>
-text \<open>So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots\<close>
+text \<open>So let's leave the \<open>Inum_C\<close> equation at the end and see what happens \dots\<close>
lemma "4 * (2 * x + (y::nat)) \<noteq> 0"
apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2 * x + (y::nat))"))
oops
-text \<open>Hm, let's specialize @{text Inum_C} with numerals.\<close>
+text \<open>Hm, let's specialize \<open>Inum_C\<close> with numerals.\<close>
lemma Inum_number: "Inum (C (numeral t)) vs = numeral t" by simp
lemmas Inum_eqs = Inum_Var Inum_Add Inum_Mul Inum_CN Inum_number
@@ -185,7 +185,7 @@
apply (reify Inum_eqs ("1 * (2 * x + (y::nat) + 0 + 1)"))
oops
-text \<open>Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "numeral"} \dots\ thing.
+text \<open>Oh!! 0 is not a variable \dots\ Oh! 0 is not a \<open>numeral\<close> \dots\ thing.
The same for 1. So let's add those equations, too.\<close>
lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
@@ -200,7 +200,7 @@
oops
text \<open>Okay, let's try reflection. Some simplifications on @{typ num} follow. You can
- skim until the main theorem @{text linum}.\<close>
+ skim until the main theorem \<open>linum\<close>.\<close>
fun lin_add :: "num \<Rightarrow> num \<Rightarrow> num"
where
--- a/src/HOL/ex/Refute_Examples.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Sat Dec 26 15:59:27 2015 +0100
@@ -15,13 +15,13 @@
lemma "P \<and> Q"
apply (rule conjI)
-refute [expect = genuine] 1 -- \<open>refutes @{term "P"}\<close>
-refute [expect = genuine] 2 -- \<open>refutes @{term "Q"}\<close>
-refute [expect = genuine] -- \<open>equivalent to 'refute 1'\<close>
- -- \<open>here 'refute 3' would cause an exception, since we only have 2 subgoals\<close>
-refute [maxsize = 5, expect = genuine] -- \<open>we can override parameters ...\<close>
+refute [expect = genuine] 1 \<comment> \<open>refutes @{term "P"}\<close>
+refute [expect = genuine] 2 \<comment> \<open>refutes @{term "Q"}\<close>
+refute [expect = genuine] \<comment> \<open>equivalent to 'refute 1'\<close>
+ \<comment> \<open>here 'refute 3' would cause an exception, since we only have 2 subgoals\<close>
+refute [maxsize = 5, expect = genuine] \<comment> \<open>we can override parameters ...\<close>
refute [satsolver = "cdclite", expect = genuine] 2
- -- \<open>... and specify a subgoal at the same time\<close>
+ \<comment> \<open>... and specify a subgoal at the same time\<close>
oops
(*****************************************************************************)
@@ -704,7 +704,7 @@
lemma "P Suc"
refute [maxsize = 3, expect = none]
--- \<open>@{term Suc} is a partial function (regardless of the size
+\<comment> \<open>@{term Suc} is a partial function (regardless of the size
of the model), hence @{term "P Suc"} is undefined and no
model will be found\<close>
oops
@@ -802,7 +802,7 @@
oops
lemma "finite x"
-refute -- \<open>no finite countermodel exists\<close>
+refute \<comment> \<open>no finite countermodel exists\<close>
oops
lemma "(x::nat) + y = 0"
--- a/src/HOL/ex/SAT_Examples.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Sat Dec 26 15:59:27 2015 +0100
@@ -277,7 +277,7 @@
(*
by sat
*)
-by rawsat -- \<open>this is without CNF conversion\<close>
+by rawsat \<comment> \<open>this is without CNF conversion\<close>
(* Translated from TPTP problem library: MSC007-1.008.dimacs *)
@@ -490,7 +490,7 @@
(*
by sat
*)
-by rawsat -- \<open>this is without CNF conversion\<close>
+by rawsat \<comment> \<open>this is without CNF conversion\<close>
(* Old sequent clause representation ("[c_i, p, ~q, \<dots>] \<turnstile> False"):
sat, zchaff_with_proofs: 8705 resolution steps in
--- a/src/HOL/ex/Set_Theory.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Set_Theory.thy Sat Dec 26 15:59:27 2015 +0100
@@ -31,14 +31,14 @@
by blast
-subsection \<open>Examples for the @{text blast} paper\<close>
+subsection \<open>Examples for the \<open>blast\<close> paper\<close>
lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
- -- \<open>Union-image, called @{text Un_Union_image} in Main HOL\<close>
+ \<comment> \<open>Union-image, called \<open>Un_Union_image\<close> in Main HOL\<close>
by blast
lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
- -- \<open>Inter-image, called @{text Int_Inter_image} in Main HOL\<close>
+ \<comment> \<open>Inter-image, called \<open>Int_Inter_image\<close> in Main HOL\<close>
by blast
lemma singleton_example_1:
@@ -47,30 +47,30 @@
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
- -- \<open>Variant of the problem above.\<close>
+ \<comment> \<open>Variant of the problem above.\<close>
by blast
lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
- -- \<open>A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail.\<close>
+ \<comment> \<open>A unique fixpoint theorem --- \<open>fast\<close>/\<open>best\<close>/\<open>meson\<close> all fail.\<close>
by metis
subsection \<open>Cantor's Theorem: There is no surjection from a set to its powerset\<close>
lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
- -- \<open>Requires best-first search because it is undirectional.\<close>
+ \<comment> \<open>Requires best-first search because it is undirectional.\<close>
by best
schematic_goal "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
- -- \<open>This form displays the diagonal term.\<close>
+ \<comment> \<open>This form displays the diagonal term.\<close>
by best
schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
- -- \<open>This form exploits the set constructs.\<close>
+ \<comment> \<open>This form exploits the set constructs.\<close>
by (rule notI, erule rangeE, best)
schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
- -- \<open>Or just this!\<close>
+ \<comment> \<open>Or just this!\<close>
by best
@@ -102,7 +102,7 @@
\<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
apply (rule decomposition [where f=f and g=g, THEN exE])
apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
- --\<open>The term above can be synthesized by a sufficiently detailed proof.\<close>
+ \<comment>\<open>The term above can be synthesized by a sufficiently detailed proof.\<close>
apply (rule bij_if_then_else)
apply (rule_tac [4] refl)
apply (rule_tac [2] inj_on_inv_into)
@@ -166,38 +166,38 @@
\<close>
lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
- -- \<open>Example 1, page 295.\<close>
+ \<comment> \<open>Example 1, page 295.\<close>
by force
lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
- -- \<open>Example 2.\<close>
+ \<comment> \<open>Example 2.\<close>
by force
lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
- -- \<open>Example 3.\<close>
+ \<comment> \<open>Example 3.\<close>
by force
lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
- -- \<open>Example 4.\<close>
- by auto --\<open>slow\<close>
+ \<comment> \<open>Example 4.\<close>
+ by auto \<comment>\<open>slow\<close>
lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
- -- \<open>Example 5, page 298.\<close>
+ \<comment> \<open>Example 5, page 298.\<close>
by force
lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
- -- \<open>Example 6.\<close>
+ \<comment> \<open>Example 6.\<close>
by force
lemma "\<exists>A. a \<notin> A"
- -- \<open>Example 7.\<close>
+ \<comment> \<open>Example 7.\<close>
by force
lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
\<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. abs y \<notin> A))"
- -- \<open>Example 8 needs a small hint.\<close>
+ \<comment> \<open>Example 8 needs a small hint.\<close>
by force
- -- \<open>not @{text blast}, which can't simplify @{text "-2 < 0"}\<close>
+ \<comment> \<open>not \<open>blast\<close>, which can't simplify \<open>-2 < 0\<close>\<close>
text \<open>Example 9 omitted (requires the reals).\<close>
@@ -205,19 +205,19 @@
lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
- -- \<open>Example 11: needs a hint.\<close>
+ \<comment> \<open>Example 11: needs a hint.\<close>
by(metis nat.induct)
lemma
"(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
\<and> P n \<longrightarrow> P m"
- -- \<open>Example 12.\<close>
+ \<comment> \<open>Example 12.\<close>
by auto
lemma
"(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
(\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
- -- \<open>Example EO1: typo in article, and with the obvious fix it seems
+ \<comment> \<open>Example EO1: typo in article, and with the obvious fix it seems
to require arithmetic reasoning.\<close>
apply clarify
apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
--- a/src/HOL/ex/Simproc_Tests.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy Sat Dec 26 15:59:27 2015 +0100
@@ -22,7 +22,7 @@
CHANGED (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs ps) 1)
\<close>
-subsection \<open>Cancellation simprocs from @{text Nat.thy}\<close>
+subsection \<open>Cancellation simprocs from \<open>Nat.thy\<close>\<close>
notepad begin
fix a b c d :: nat
@@ -59,7 +59,7 @@
end
(* TODO: more tests for Groups.group_cancel_{add,diff,eq,less,le} *)
-subsection \<open>@{text int_combine_numerals}\<close>
+subsection \<open>\<open>int_combine_numerals\<close>\<close>
(* FIXME: int_combine_numerals often unnecessarily regroups addition
and rewrites subtraction to negation. Ideally it should behave more
@@ -128,7 +128,7 @@
}
end
-subsection \<open>@{text inteq_cancel_numerals}\<close>
+subsection \<open>\<open>inteq_cancel_numerals\<close>\<close>
notepad begin
fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1"
@@ -151,7 +151,7 @@
}
end
-subsection \<open>@{text intless_cancel_numerals}\<close>
+subsection \<open>\<open>intless_cancel_numerals\<close>\<close>
notepad begin
fix b c i j k u y :: "'a::linordered_idom"
@@ -172,7 +172,7 @@
}
end
-subsection \<open>@{text ring_eq_cancel_numeral_factor}\<close>
+subsection \<open>\<open>ring_eq_cancel_numeral_factor\<close>\<close>
notepad begin
fix x y :: "'a::{idom,ring_char_0}"
@@ -197,7 +197,7 @@
}
end
-subsection \<open>@{text int_div_cancel_numeral_factors}\<close>
+subsection \<open>\<open>int_div_cancel_numeral_factors\<close>\<close>
notepad begin
fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
@@ -220,7 +220,7 @@
}
end
-subsection \<open>@{text ring_less_cancel_numeral_factor}\<close>
+subsection \<open>\<open>ring_less_cancel_numeral_factor\<close>\<close>
notepad begin
fix x y :: "'a::linordered_idom"
@@ -245,7 +245,7 @@
}
end
-subsection \<open>@{text ring_le_cancel_numeral_factor}\<close>
+subsection \<open>\<open>ring_le_cancel_numeral_factor\<close>\<close>
notepad begin
fix x y :: "'a::linordered_idom"
@@ -276,7 +276,7 @@
}
end
-subsection \<open>@{text divide_cancel_numeral_factor}\<close>
+subsection \<open>\<open>divide_cancel_numeral_factor\<close>\<close>
notepad begin
fix x y z :: "'a::{field,ring_char_0}"
@@ -298,7 +298,7 @@
}
end
-subsection \<open>@{text ring_eq_cancel_factor}\<close>
+subsection \<open>\<open>ring_eq_cancel_factor\<close>\<close>
notepad begin
fix a b c d k x y :: "'a::idom"
@@ -323,7 +323,7 @@
}
end
-subsection \<open>@{text int_div_cancel_factor}\<close>
+subsection \<open>\<open>int_div_cancel_factor\<close>\<close>
notepad begin
fix a b c d k uu x y :: "'a::semiring_div"
@@ -347,9 +347,9 @@
end
lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field)*(x*a)/z"
-oops -- "FIXME: need simproc to cover this case"
+oops \<comment> "FIXME: need simproc to cover this case"
-subsection \<open>@{text divide_cancel_factor}\<close>
+subsection \<open>\<open>divide_cancel_factor\<close>\<close>
notepad begin
fix a b c d k uu x y :: "'a::field"
@@ -375,9 +375,9 @@
lemma
fixes a b c d x y z :: "'a::linordered_field"
shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
-oops -- "FIXME: need simproc to cover this case"
+oops \<comment> "FIXME: need simproc to cover this case"
-subsection \<open>@{text linordered_ring_less_cancel_factor}\<close>
+subsection \<open>\<open>linordered_ring_less_cancel_factor\<close>\<close>
notepad begin
fix x y z :: "'a::linordered_idom"
@@ -404,7 +404,7 @@
}
end
-subsection \<open>@{text linordered_ring_le_cancel_factor}\<close>
+subsection \<open>\<open>linordered_ring_le_cancel_factor\<close>\<close>
notepad begin
fix x y z :: "'a::linordered_idom"
@@ -417,7 +417,7 @@
}
end
-subsection \<open>@{text field_combine_numerals}\<close>
+subsection \<open>\<open>field_combine_numerals\<close>\<close>
notepad begin
fix x y z uu :: "'a::{field,ring_char_0}"
@@ -445,9 +445,9 @@
fixes x :: "'a::{linordered_field}"
shows "2/3 * x + x / 3 = uu"
apply (tactic \<open>test @{context} [@{simproc field_combine_numerals}]\<close>)?
-oops -- "FIXME: test fails"
+oops \<comment> "FIXME: test fails"
-subsection \<open>@{text nat_combine_numerals}\<close>
+subsection \<open>\<open>nat_combine_numerals\<close>\<close>
notepad begin
fix i j k m n u :: nat
@@ -475,7 +475,7 @@
}
end
-subsection \<open>@{text nateq_cancel_numerals}\<close>
+subsection \<open>\<open>nateq_cancel_numerals\<close>\<close>
notepad begin
fix i j k l oo u uu vv w y z w' y' z' :: "nat"
@@ -522,7 +522,7 @@
}
end
-subsection \<open>@{text natless_cancel_numerals}\<close>
+subsection \<open>\<open>natless_cancel_numerals\<close>\<close>
notepad begin
fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a"
@@ -543,7 +543,7 @@
}
end
-subsection \<open>@{text natle_cancel_numerals}\<close>
+subsection \<open>\<open>natle_cancel_numerals\<close>\<close>
notepad begin
fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
@@ -570,7 +570,7 @@
}
end
-subsection \<open>@{text natdiff_cancel_numerals}\<close>
+subsection \<open>\<open>natdiff_cancel_numerals\<close>\<close>
notepad begin
fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
@@ -630,9 +630,9 @@
subsection \<open>Factor-cancellation simprocs for type @{typ nat}\<close>
-text \<open>@{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
-@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
-@{text nat_dvd_cancel_factor}.\<close>
+text \<open>\<open>nat_eq_cancel_factor\<close>, \<open>nat_less_cancel_factor\<close>,
+\<open>nat_le_cancel_factor\<close>, \<open>nat_divide_cancel_factor\<close>, and
+\<open>nat_dvd_cancel_factor\<close>.\<close>
notepad begin
fix a b c d k x y uu :: nat
--- a/src/HOL/ex/Sqrt_Script.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Sqrt_Script.thy Sat Dec 26 15:59:27 2015 +0100
@@ -52,7 +52,7 @@
subsection \<open>Main theorem\<close>
text \<open>
- The square root of any prime number (including @{text 2}) is
+ The square root of any prime number (including \<open>2\<close>) is
irrational.
\<close>
--- a/src/HOL/ex/Sudoku.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Sudoku.thy Sat Dec 26 15:59:27 2015 +0100
@@ -12,9 +12,9 @@
text \<open>
See the paper ``A SAT-based Sudoku Solver'' (Tjark Weber, published at
LPAR'05) for further explanations. (The paper describes an older version of
- this theory that used the model finder @{text refute} to find Sudoku
- solutions. The @{text refute} tool has since been superseded by
- @{text nitpick}, which is used below.)
+ this theory that used the model finder \<open>refute\<close> to find Sudoku
+ solutions. The \<open>refute\<close> tool has since been superseded by
+ \<open>nitpick\<close>, which is used below.)
\<close>
no_notation Groups.one_class.one ("1")
--- a/src/HOL/ex/Tarski.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Tarski.thy Sat Dec 26 15:59:27 2015 +0100
@@ -196,13 +196,13 @@
"S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder"
apply (simp (no_asm) add: PartialOrder_def)
apply auto
--- \<open>refl\<close>
+\<comment> \<open>refl\<close>
apply (simp add: refl_on_def induced_def)
apply (blast intro: reflE)
--- \<open>antisym\<close>
+\<comment> \<open>antisym\<close>
apply (simp add: antisym_def induced_def)
apply (blast intro: antisymE)
--- \<open>trans\<close>
+\<comment> \<open>trans\<close>
apply (simp add: trans_def induced_def)
apply (blast intro: transE)
done
@@ -441,7 +441,7 @@
text \<open>
Reduce the sublattice property by using substructural properties;
- abandoned see @{text "Tarski_4.ML"}.
+ abandoned see \<open>Tarski_4.ML\<close>.
\<close>
lemma (in CLF) [simp]:
@@ -490,13 +490,13 @@
apply (rule lub_least, fast)
apply (rule f_in_funcset [THEN funcset_mem])
apply (rule lub_in_lattice, fast)
--- \<open>@{text "\<forall>x:H. (x, f (lub H r)) \<in> r"}\<close>
+\<comment> \<open>\<open>\<forall>x:H. (x, f (lub H r)) \<in> r\<close>\<close>
apply (rule ballI)
apply (rule transE)
--- \<open>instantiates @{text "(x, ???z) \<in> order cl to (x, f x)"},\<close>
--- \<open>because of the def of @{text H}\<close>
+\<comment> \<open>instantiates \<open>(x, ???z) \<in> order cl to (x, f x)\<close>,\<close>
+\<comment> \<open>because of the def of \<open>H\<close>\<close>
apply fast
--- \<open>so it remains to show @{text "(f x, f (lub H cl)) \<in> r"}\<close>
+\<comment> \<open>so it remains to show \<open>(f x, f (lub H cl)) \<in> r\<close>\<close>
apply (rule_tac f = "f" in monotoneE)
apply (rule monotone_f, fast)
apply (rule lub_in_lattice, fast)
@@ -564,7 +564,7 @@
done
lemma (in CLF) glbH_is_fixp: "H = {x. (f x, x) \<in> r & x \<in> A} ==> glb H cl \<in> P"
- -- \<open>Tarski for glb\<close>
+ \<comment> \<open>Tarski for glb\<close>
apply (simp add: glb_dual_lub P_def A_def r_def)
apply (rule dualA_iff [THEN subst])
apply (rule CLF.lubH_is_fixp)
@@ -627,7 +627,7 @@
apply (rule ballI)
apply (simp add: interval_lemma1)
apply (simp add: isLub_upper)
--- \<open>@{text "(L, b) \<in> r"}\<close>
+\<comment> \<open>\<open>(L, b) \<in> r\<close>\<close>
apply (simp add: isLub_least interval_lemma2)
done
@@ -657,38 +657,38 @@
prefer 2 apply assumption
apply assumption
apply (erule exE)
--- \<open>define the lub for the interval as\<close>
+\<comment> \<open>define the lub for the interval as\<close>
apply (rule_tac x = "if S = {} then a else L" in exI)
apply (simp (no_asm_simp) add: isLub_def split del: split_if)
apply (intro impI conjI)
--- \<open>@{text "(if S = {} then a else L) \<in> interval r a b"}\<close>
+\<comment> \<open>\<open>(if S = {} then a else L) \<in> interval r a b\<close>\<close>
apply (simp add: CL_imp_PO L_in_interval)
apply (simp add: left_in_interval)
--- \<open>lub prop 1\<close>
+\<comment> \<open>lub prop 1\<close>
apply (case_tac "S = {}")
--- \<open>@{text "S = {}, y \<in> S = False => everything"}\<close>
+\<comment> \<open>\<open>S = {}, y \<in> S = False => everything\<close>\<close>
apply fast
--- \<open>@{text "S \<noteq> {}"}\<close>
+\<comment> \<open>\<open>S \<noteq> {}\<close>\<close>
apply simp
--- \<open>@{text "\<forall>y:S. (y, L) \<in> induced (interval r a b) r"}\<close>
+\<comment> \<open>\<open>\<forall>y:S. (y, L) \<in> induced (interval r a b) r\<close>\<close>
apply (rule ballI)
apply (simp add: induced_def L_in_interval)
apply (rule conjI)
apply (rule subsetD)
apply (simp add: S_intv_cl, assumption)
apply (simp add: isLub_upper)
--- \<open>@{text "\<forall>z:interval r a b. (\<forall>y:S. (y, z) \<in> induced (interval r a b) r \<longrightarrow> (if S = {} then a else L, z) \<in> induced (interval r a b) r"}\<close>
+\<comment> \<open>\<open>\<forall>z:interval r a b. (\<forall>y:S. (y, z) \<in> induced (interval r a b) r \<longrightarrow> (if S = {} then a else L, z) \<in> induced (interval r a b) r\<close>\<close>
apply (rule ballI)
apply (rule impI)
apply (case_tac "S = {}")
--- \<open>@{text "S = {}"}\<close>
+\<comment> \<open>\<open>S = {}\<close>\<close>
apply simp
apply (simp add: induced_def interval_def)
apply (rule conjI)
apply (rule reflE, assumption)
apply (rule interval_not_empty)
apply (simp add: interval_def)
--- \<open>@{text "S \<noteq> {}"}\<close>
+\<comment> \<open>\<open>S \<noteq> {}\<close>\<close>
apply simp
apply (simp add: induced_def L_in_interval)
apply (rule isLub_least, assumption)
@@ -785,11 +785,11 @@
apply (rule Y_subset_A)
apply (rule f_in_funcset [THEN funcset_mem])
apply (rule lubY_in_A)
--- \<open>@{text "Y \<subseteq> P ==> f x = x"}\<close>
+\<comment> \<open>\<open>Y \<subseteq> P ==> f x = x\<close>\<close>
apply (rule ballI)
apply (rule_tac t = "x" in fix_imp_eq [THEN subst])
apply (erule Y_ss [simplified P_def, THEN subsetD])
--- \<open>@{text "reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r"} by monotonicity\<close>
+\<comment> \<open>\<open>reduce (f x, f (lub Y cl)) \<in> r to (x, lub Y cl) \<in> r\<close> by monotonicity\<close>
apply (rule_tac f = "f" in monotoneE)
apply (rule monotone_f)
apply (simp add: Y_subset_A [THEN subsetD])
@@ -811,13 +811,13 @@
apply (rule conjI)
apply (rule transE)
apply (rule lubY_le_flubY)
--- \<open>@{text "(f (lub Y cl), f x) \<in> r"}\<close>
+\<comment> \<open>\<open>(f (lub Y cl), f x) \<in> r\<close>\<close>
apply (rule_tac f=f in monotoneE)
apply (rule monotone_f)
apply (rule lubY_in_A)
apply (simp add: intY1_def interval_def intY1_elem)
apply (simp add: intY1_def interval_def)
--- \<open>@{text "(f x, Top cl) \<in> r"}\<close>
+\<comment> \<open>\<open>(f x, Top cl) \<in> r\<close>\<close>
apply (rule Top_prop)
apply (rule f_in_funcset [THEN funcset_mem])
apply (simp add: intY1_def interval_def intY1_elem)
@@ -874,11 +874,11 @@
"\<exists>L. isLub Y (| pset = P, order = induced P r |) L"
apply (rule_tac x = "v" in exI)
apply (simp add: isLub_def)
--- \<open>@{text "v \<in> P"}\<close>
+\<comment> \<open>\<open>v \<in> P\<close>\<close>
apply (simp add: v_in_P)
apply (rule conjI)
--- \<open>@{text v} is lub\<close>
--- \<open>@{text "1. \<forall>y:Y. (y, v) \<in> induced P r"}\<close>
+\<comment> \<open>\<open>v\<close> is lub\<close>
+\<comment> \<open>\<open>1. \<forall>y:Y. (y, v) \<in> induced P r\<close>\<close>
apply (rule ballI)
apply (simp add: induced_def subsetD v_in_P)
apply (rule conjI)
--- a/src/HOL/ex/Termination.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Termination.thy Sat Dec 26 15:59:27 2015 +0100
@@ -9,7 +9,7 @@
imports Main "~~/src/HOL/Library/Multiset"
begin
-subsection \<open>Manually giving termination relations using @{text relation} and
+subsection \<open>Manually giving termination relations using \<open>relation\<close> and
@{term measure}\<close>
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -29,10 +29,10 @@
termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
-subsection \<open>@{text lexicographic_order}: Trivial examples\<close>
+subsection \<open>\<open>lexicographic_order\<close>: Trivial examples\<close>
text \<open>
- The @{text fun} command uses the method @{text lexicographic_order} by default,
+ The \<open>fun\<close> command uses the method \<open>lexicographic_order\<close> by default,
so it is not explicitly invoked.
\<close>
@@ -168,9 +168,9 @@
-subsection \<open>Refined analysis: The @{text size_change} method\<close>
+subsection \<open>Refined analysis: The \<open>size_change\<close> method\<close>
-text \<open>Unsolvable for @{text lexicographic_order}\<close>
+text \<open>Unsolvable for \<open>lexicographic_order\<close>\<close>
function fun1 :: "nat * nat \<Rightarrow> nat"
where
@@ -183,7 +183,7 @@
text \<open>
- @{text lexicographic_order} can do the following, but it is much slower.
+ \<open>lexicographic_order\<close> can do the following, but it is much slower.
\<close>
function
@@ -227,7 +227,7 @@
0
)"
by pat_completeness auto
-termination by size_change -- \<open>requires Multiset\<close>
+termination by size_change \<comment> \<open>requires Multiset\<close>
definition negate :: "int \<Rightarrow> int"
where "negate i = - i"
--- a/src/HOL/ex/ThreeDivides.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/ThreeDivides.thy Sat Dec 26 15:59:27 2015 +0100
@@ -23,7 +23,7 @@
sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j
- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$,
therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
-@{text "\<box>"}
+\<open>\<box>\<close>
\<close>
@@ -31,8 +31,8 @@
subsubsection \<open>Miscellaneous summation lemmas\<close>
-text \<open>If $a$ divides @{text "A x"} for all x then $a$ divides any
-sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$.\<close>
+text \<open>If $a$ divides \<open>A x\<close> for all x then $a$ divides any
+sum over terms of the form \<open>(A x)*(P x)\<close> for arbitrary $P$.\<close>
lemma div_sum:
fixes a::nat and n::nat
@@ -84,14 +84,14 @@
thus ?case by simp
qed
-text \<open>Expanding on the previous lemma and lemma @{text "div_sum"}.\<close>
+text \<open>Expanding on the previous lemma and lemma \<open>div_sum\<close>.\<close>
lemma three_divs_1:
fixes D :: "nat \<Rightarrow> nat"
shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"
by (subst mult.commute, rule div_sum) (simp add: three_divs_0 [simplified])
-text \<open>Using lemmas @{text "digit_diff_split"} and
-@{text "three_divs_1"} we now prove the following lemma.
+text \<open>Using lemmas \<open>digit_diff_split\<close> and
+\<open>three_divs_1\<close> we now prove the following lemma.
\<close>
lemma three_divs_2:
fixes nd::nat and D::"nat\<Rightarrow>nat"
@@ -136,8 +136,7 @@
text \<open>This section shows that for all natural numbers we can
generate a sequence of digits less than ten that represent the decimal
-expansion of the number. We then use the lemma @{text
-"three_div_general"} to prove our final theorem.\<close>
+expansion of the number. We then use the lemma \<open>three_div_general\<close> to prove our final theorem.\<close>
text \<open>\medskip Definitions of length and digit sum.\<close>
@@ -146,7 +145,7 @@
required properties of natural numbers. We then proceed to prove some
properties of these functions.
-The function @{text "nlen"} returns the number of digits in a natural
+The function \<open>nlen\<close> returns the number of digits in a natural
number n.\<close>
fun nlen :: "nat \<Rightarrow> nat"
@@ -154,7 +153,7 @@
"nlen 0 = 0"
| "nlen x = 1 + nlen (x div 10)"
-text \<open>The function @{text "sumdig"} returns the sum of all digits in
+text \<open>The function \<open>sumdig\<close> returns the sum of all digits in
some number n.\<close>
definition
@@ -214,8 +213,8 @@
text \<open>\medskip Final theorem.\<close>
-text \<open>We now combine the general theorem @{text "three_div_general"}
-and existence result of @{text "exp_exists"} to prove our final
+text \<open>We now combine the general theorem \<open>three_div_general\<close>
+and existence result of \<open>exp_exists\<close> to prove our final
theorem.\<close>
theorem three_divides_nat:
--- a/src/HOL/ex/Transfer_Int_Nat.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Sat Dec 26 15:59:27 2015 +0100
@@ -114,7 +114,7 @@
apply simp_all
done
-text \<open>For derived operations, we can use the @{text "transfer_prover"}
+text \<open>For derived operations, we can use the \<open>transfer_prover\<close>
method to help generate transfer rules.\<close>
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
@@ -159,8 +159,8 @@
apply fact
done
-text \<open>The @{text "fixing"} option prevents generalization over the free
- variable @{text "n"}, allowing the local transfer rule to be used.\<close>
+text \<open>The \<open>fixing\<close> option prevents generalization over the free
+ variable \<open>n\<close>, allowing the local transfer rule to be used.\<close>
lemma
assumes [transfer_rule]: "ZN x n"
@@ -185,7 +185,7 @@
apply fact
done
-text \<open>Quantifiers over higher types (e.g. @{text "nat list"}) are
+text \<open>Quantifiers over higher types (e.g. \<open>nat list\<close>) are
transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\<close>
lemma
--- a/src/HOL/ex/Tree23.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Tree23.thy Sat Dec 26 15:59:27 2015 +0100
@@ -19,7 +19,7 @@
function definitions take a few minutes and can also be seen as stress tests
for the function definition facility.\<close>
-type_synonym key = int -- \<open>for simplicity, should be a type class\<close>
+type_synonym key = int \<comment> \<open>for simplicity, should be a type class\<close>
datatype ord = LESS | EQUAL | GREATER
--- a/src/HOL/ex/Unification.thy Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Unification.thy Sat Dec 26 15:59:27 2015 +0100
@@ -379,17 +379,17 @@
show "wf ?R" by simp
fix M N M' N' :: "'a trm"
- show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
+ show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" \<comment> "Inner call"
by (rule measures_lesseq) (auto intro: card_mono)
- fix \<theta> -- "Outer call"
+ fix \<theta> \<comment> "Outer call"
assume inner: "unify_dom (M, M')"
"unify M M' = Some \<theta>"
from unify_eliminates[OF inner]
show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
proof
- -- \<open>Either a variable is eliminated \ldots\<close>
+ \<comment> \<open>Either a variable is eliminated \ldots\<close>
assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
then obtain v
where "elim \<theta> v"
@@ -402,7 +402,7 @@
thus ?thesis
by (auto intro!: measures_less intro: psubset_card_mono)
next
- -- \<open>Or the substitution is empty\<close>
+ \<comment> \<open>Or the substitution is empty\<close>
assume "\<theta> \<doteq> []"
hence "N \<lhd> \<theta> = N"
and "N' \<lhd> \<theta> = N'" by auto
@@ -417,7 +417,7 @@
lemma unify_computes_MGU:
"unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
- case (7 M N M' N' \<sigma>) -- "The interesting case"
+ case (7 M N M' N' \<sigma>) \<comment> "The interesting case"
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \<theta>1"