--- a/src/Doc/Implementation/Eq.thy Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Implementation/Eq.thy Tue Oct 20 23:53:40 2015 +0200
@@ -6,7 +6,7 @@
text \<open>Equality is one of the most fundamental concepts of
mathematics. The Isabelle/Pure logic (\chref{ch:logic}) provides a
- builtin relation @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} that expresses equality
+ builtin relation \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> that expresses equality
of arbitrary terms (or propositions) at the framework level, as
expressed by certain basic inference rules (\secref{sec:eq-rules}).
@@ -18,7 +18,7 @@
Higher-order matching is able to provide suitable instantiations for
giving equality rules, which leads to the versatile concept of
- @{text "\<lambda>"}-term rewriting (\secref{sec:rewriting}). Internally
+ \<open>\<lambda>\<close>-term rewriting (\secref{sec:rewriting}). Internally
this is based on the general-purpose Simplifier engine of Isabelle,
which is more specific and more efficient than plain conversions.
@@ -31,10 +31,10 @@
section \<open>Basic equality rules \label{sec:eq-rules}\<close>
-text \<open>Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary
+text \<open>Isabelle/Pure uses \<open>\<equiv>\<close> for equality of arbitrary
terms, which includes equivalence of propositions of the logical
- framework. The conceptual axiomatization of the constant @{text "\<equiv>
- :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} is given in \figref{fig:pure-equality}. The
+ framework. The conceptual axiomatization of the constant \<open>\<equiv>
+ :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> is given in \figref{fig:pure-equality}. The
inference kernel presents slightly different equality rules, which
may be understood as derived rules from this minimal axiomatization.
The Pure theory also provides some theorems that express the same
@@ -42,15 +42,14 @@
rules as explained in \secref{sec:obj-rules}.
For example, @{ML Thm.symmetric} as Pure inference is an ML function
- that maps a theorem @{text "th"} stating @{text "t \<equiv> u"} to one
- stating @{text "u \<equiv> t"}. In contrast, @{thm [source]
+ that maps a theorem \<open>th\<close> stating \<open>t \<equiv> u\<close> to one
+ stating \<open>u \<equiv> t\<close>. In contrast, @{thm [source]
Pure.symmetric} as Pure theorem expresses the same reasoning in
- declarative form. If used like @{text "th [THEN Pure.symmetric]"}
+ declarative form. If used like \<open>th [THEN Pure.symmetric]\<close>
in Isar source notation, it achieves a similar effect as the ML
inference function, although the rule attribute @{attribute THEN} or
ML operator @{ML "op RS"} involve the full machinery of higher-order
- unification (modulo @{text "\<beta>\<eta>"}-conversion) and lifting of @{text
- "\<And>/\<Longrightarrow>"} contexts.\<close>
+ unification (modulo \<open>\<beta>\<eta>\<close>-conversion) and lifting of \<open>\<And>/\<Longrightarrow>\<close> contexts.\<close>
text %mlref \<open>
\begin{mldecls}
@@ -64,8 +63,8 @@
\end{mldecls}
See also @{file "~~/src/Pure/thm.ML" } for further description of
- these inference rules, and a few more for primitive @{text "\<beta>"} and
- @{text "\<eta>"} conversions. Note that @{text "\<alpha>"} conversion is
+ these inference rules, and a few more for primitive \<open>\<beta>\<close> and
+ \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close> conversion is
implicit due to the representation of terms with de-Bruijn indices
(\secref{sec:terms}).\<close>
@@ -83,10 +82,10 @@
section \<open>Rewriting \label{sec:rewriting}\<close>
text \<open>Rewriting normalizes a given term (theorem or goal) by
- replacing instances of given equalities @{text "t \<equiv> u"} in subterms.
+ replacing instances of given equalities \<open>t \<equiv> u\<close> in subterms.
Rewriting continues until no rewrites are applicable to any subterm.
- This may be used to unfold simple definitions of the form @{text "f
- x\<^sub>1 \<dots> x\<^sub>n \<equiv> u"}, but is slightly more general than that.
+ This may be used to unfold simple definitions of the form \<open>f
+ x\<^sub>1 \<dots> x\<^sub>n \<equiv> u\<close>, but is slightly more general than that.
\<close>
text %mlref \<open>
@@ -98,23 +97,22 @@
@{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
\end{mldecls}
- \<^descr> @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
+ \<^descr> @{ML rewrite_rule}~\<open>ctxt rules thm\<close> rewrites the whole
theorem by the given rules.
- \<^descr> @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
+ \<^descr> @{ML rewrite_goals_rule}~\<open>ctxt rules thm\<close> rewrites the
outer premises of the given theorem. Interpreting the same as a
goal state (\secref{sec:tactical-goals}) it means to rewrite all
subgoals (in the same manner as @{ML rewrite_goals_tac}).
- \<^descr> @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
- @{text "i"} by the given rewrite rules.
+ \<^descr> @{ML rewrite_goal_tac}~\<open>ctxt rules i\<close> rewrites subgoal
+ \<open>i\<close> by the given rewrite rules.
- \<^descr> @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
+ \<^descr> @{ML rewrite_goals_tac}~\<open>ctxt rules\<close> rewrites all subgoals
by the given rewrite rules.
- \<^descr> @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
- rewrite_goals_tac} with the symmetric form of each member of @{text
- "rules"}, re-ordered to fold longer expression first. This supports
+ \<^descr> @{ML fold_goals_tac}~\<open>ctxt rules\<close> essentially uses @{ML
+ rewrite_goals_tac} with the symmetric form of each member of \<open>rules\<close>, re-ordered to fold longer expression first. This supports
to idea to fold primitive definitions that appear in expended form
in the proof state.
\<close>