summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 10 Apr 2016 23:15:34 +0200 | |

changeset 62947 | 3374f3ffb2ec |

parent 62946 | 9f537dd83677 |

child 62948 | 7700f467892b |

child 62952 | 85c6c2a1952d |

tuned;

--- 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