# HG changeset patch
# User wenzelm
# Date 1460322934 -7200
# Node ID 3374f3ffb2ec77daf30e6e2f7e26460232583534
# Parent  9f537dd836772b1825e97a41f956d7bf62b311c1
tuned;

diff -r 9f537dd83677 -r 3374f3ffb2ec src/Doc/Implementation/Integration.thy
--- 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
diff -r 9f537dd83677 -r 3374f3ffb2ec src/HOL/Library/BigO.thy
--- 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>
diff -r 9f537dd83677 -r 3374f3ffb2ec src/HOL/Statespace/StateSpaceEx.thy
--- 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