--- a/src/Doc/Isar_Ref/Framework.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Fri Aug 12 17:53:55 2016 +0200
@@ -89,13 +89,13 @@
\<^medskip>
Concrete applications require another intermediate layer: an object-logic.
Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
- commonly used; elementary examples are given in the directory @{dir
- "~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh
+ commonly used; elementary examples are given in the directory
+ \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh
object-logic from Isabelle/Pure, and use Isar proofs from the very start,
despite the lack of advanced proof tools at such an early stage (e.g.\ see
- @{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL
- @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work,
- but are much less developed.
+ \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
+ "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
+ much less developed.
In order to illustrate natural deduction in Isar, we shall subsequently
refer to the background theory and library of Isabelle/HOL. This includes
@@ -524,7 +524,7 @@
may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
methods semantically in Isabelle/ML. The Eisbach language allows to define
proof methods symbolically, as recursive expressions over existing methods
- @{cite "Matichuk-et-al:2014"}; see also @{dir "~~/src/HOL/Eisbach"}.
+ @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''