--- a/src/Doc/Implementation/Integration.thy Sun Apr 10 22:27:43 2016 +0200
+++ b/src/Doc/Implementation/Integration.thy Sun Apr 10 23:15:34 2016 +0200
@@ -84,8 +84,8 @@
The operational part is represented as the sequential union of a list of
partial functions, which are tried in turn until the first one succeeds.
This acts like an outer case-expression for various alternative state
- transitions. For example, \isakeyword{qed} works differently for a local
- proofs vs.\ the global ending of an outermost proof.
+ transitions. For example, \<^theory_text>\<open>qed\<close> works differently for a local proofs vs.\
+ the global ending of an outermost proof.
Transitions are composed via transition transformers. Internally, Isar
commands are put together from an empty transition extended by name and
--- a/src/HOL/Library/BigO.thy Sun Apr 10 22:27:43 2016 +0200
+++ b/src/HOL/Library/BigO.thy Sun Apr 10 23:15:34 2016 +0200
@@ -29,7 +29,7 @@
inclusion, to use the automated reasoners effectively with the library
one should redeclare the theorem \<open>subsetI\<close> as an intro rule,
rather than as an \<open>intro!\<close> rule, for example, using
-\isa{\isakeyword{declare}}~\<open>subsetI [del, intro]\<close>.
+\<^theory_text>\<open>declare subsetI [del, intro]\<close>.
\<close>
subsection \<open>Definitions\<close>
--- a/src/HOL/Statespace/StateSpaceEx.thy Sun Apr 10 22:27:43 2016 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy Sun Apr 10 23:15:34 2016 +0200
@@ -19,7 +19,7 @@
text {* Isabelle allows to add new top-level commands to the
system. Building on the locale infrastructure, we provide a command
-\isacommand{statespace} like this:*}
+\<^theory_text>\<open>statespace\<close> like this:*}
statespace vars =
n::nat
@@ -29,7 +29,7 @@
print_locale vars_valuetypes
print_locale vars
-text {* \noindent This resembles a \isacommand{record} definition,
+text {* \noindent This resembles a \<^theory_text>\<open>record\<close> definition,
but introduces sophisticated locale
infrastructure instead of HOL type schemes. The resulting context
postulates two distinct names @{term "n"} and @{term "b"} and