isabelle update_cartouches -t;
authorwenzelm
Thu Nov 08 22:29:09 2018 +0100 (9 months ago)
changeset 6927215e9ed5b28fb
parent 69271 4cb70e7e36b9
child 69273 e86d8cb40610
isabelle update_cartouches -t;
src/Benchmarks/ROOT
src/CCL/ROOT
src/CTT/ROOT
src/Cube/ROOT
src/FOL/ROOT
src/FOLP/ROOT
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Eisbach/Eisbach.thy
src/HOL/Filter.thy
src/HOL/Library/Code_Lazy.thy
src/HOL/Library/IArray.thy
src/HOL/Library/Landau_Symbols.thy
src/HOL/Limits.thy
src/HOL/ROOT
src/HOL/String.thy
src/HOL/Transcendental.thy
src/LCF/ROOT
src/Pure/ROOT
src/Sequents/ROOT
src/ZF/ROOT
     1.1 --- a/src/Benchmarks/ROOT	Thu Nov 08 22:02:07 2018 +0100
     1.2 +++ b/src/Benchmarks/ROOT	Thu Nov 08 22:29:09 2018 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  chapter HOL
     1.5  
     1.6  session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" +
     1.7 -  description {*
     1.8 +  description \<open>
     1.9      Big (co)datatypes.
    1.10 -  *}
    1.11 +\<close>
    1.12    theories
    1.13      Brackin
    1.14      IsaFoR
    1.15 @@ -17,8 +17,8 @@
    1.16      Needham_Schroeder_Unguided_Attacker_Example
    1.17  
    1.18  session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
    1.19 -  description {*
    1.20 +  description \<open>
    1.21      Big records.
    1.22 -  *}
    1.23 +\<close>
    1.24    theories
    1.25      Record_Benchmark
     2.1 --- a/src/CCL/ROOT	Thu Nov 08 22:02:07 2018 +0100
     2.2 +++ b/src/CCL/ROOT	Thu Nov 08 22:29:09 2018 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  chapter CCL
     2.5  
     2.6  session CCL = Pure +
     2.7 -  description {*
     2.8 +  description \<open>
     2.9      Author:     Martin Coen, Cambridge University Computer Laboratory
    2.10      Copyright   1993  University of Cambridge
    2.11  
    2.12 @@ -9,7 +9,7 @@
    2.13  
    2.14      A computational logic for an untyped functional language with
    2.15      evaluation to weak head-normal form.
    2.16 -  *}
    2.17 +\<close>
    2.18    sessions
    2.19      FOL
    2.20    theories
     3.1 --- a/src/CTT/ROOT	Thu Nov 08 22:02:07 2018 +0100
     3.2 +++ b/src/CTT/ROOT	Thu Nov 08 22:29:09 2018 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  chapter CTT
     3.5  
     3.6  session CTT = Pure +
     3.7 -  description {*
     3.8 +  description \<open>
     3.9      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.10      Copyright   1991  University of Cambridge
    3.11  
    3.12 @@ -15,7 +15,7 @@
    3.13  
    3.14      Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
    3.15      1991)
    3.16 -  *}
    3.17 +\<close>
    3.18    options [thy_output_source]
    3.19    theories
    3.20      CTT
     4.1 --- a/src/Cube/ROOT	Thu Nov 08 22:02:07 2018 +0100
     4.2 +++ b/src/Cube/ROOT	Thu Nov 08 22:29:09 2018 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  chapter Cube
     4.5  
     4.6  session Cube = Pure +
     4.7 -  description {*
     4.8 +  description \<open>
     4.9      Author:     Tobias Nipkow
    4.10      Copyright   1992  University of Cambridge
    4.11  
    4.12 @@ -12,5 +12,5 @@
    4.13  
    4.14      For more information about the Lambda-Cube, see H. Barendregt, Introduction
    4.15      to Generalised Type Systems, J. Functional Programming.
    4.16 -  *}
    4.17 +\<close>
    4.18    theories Example
     5.1 --- a/src/FOL/ROOT	Thu Nov 08 22:02:07 2018 +0100
     5.2 +++ b/src/FOL/ROOT	Thu Nov 08 22:29:09 2018 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  chapter FOL
     5.5  
     5.6  session FOL = Pure +
     5.7 -  description {*
     5.8 +  description \<open>
     5.9      First-Order Logic with Natural Deduction (constructive and classical
    5.10      versions). For a classical sequent calculus, see Isabelle/LK.
    5.11  
    5.12 @@ -14,16 +14,16 @@
    5.13      Antony Galton, Logic for Information Technology (Wiley, 1990)
    5.14  
    5.15      Michael Dummett, Elements of Intuitionism (Oxford, 1977)
    5.16 -  *}
    5.17 +\<close>
    5.18    theories
    5.19      IFOL (global)
    5.20      FOL (global)
    5.21    document_files "root.tex"
    5.22  
    5.23  session "FOL-ex" in ex = FOL +
    5.24 -  description {*
    5.25 +  description \<open>
    5.26      Examples for First-Order Logic.
    5.27 -  *}
    5.28 +\<close>
    5.29    theories
    5.30      Natural_Numbers
    5.31      Intro
     6.1 --- a/src/FOLP/ROOT	Thu Nov 08 22:02:07 2018 +0100
     6.2 +++ b/src/FOLP/ROOT	Thu Nov 08 22:29:09 2018 +0100
     6.3 @@ -1,25 +1,25 @@
     6.4  chapter FOLP
     6.5  
     6.6  session FOLP = Pure +
     6.7 -  description {*
     6.8 +  description \<open>
     6.9      Author:     Martin Coen, Cambridge University Computer Laboratory
    6.10      Copyright   1993  University of Cambridge
    6.11  
    6.12      Modifed version of FOL that contains proof terms.
    6.13  
    6.14      Presence of unknown proof term means that matching does not behave as expected.
    6.15 -  *}
    6.16 +\<close>
    6.17    theories
    6.18      IFOLP (global)
    6.19      FOLP (global)
    6.20  
    6.21  session "FOLP-ex" in ex = FOLP +
    6.22 -  description {*
    6.23 +  description \<open>
    6.24      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    6.25      Copyright   1992  University of Cambridge
    6.26  
    6.27      Examples for First-Order Logic.
    6.28 -  *}
    6.29 +\<close>
    6.30    theories
    6.31      Intro
    6.32      Nat
     7.1 --- a/src/HOL/Algebra/Group.thy	Thu Nov 08 22:02:07 2018 +0100
     7.2 +++ b/src/HOL/Algebra/Group.thy	Thu Nov 08 22:29:09 2018 +0100
     7.3 @@ -1394,7 +1394,7 @@
     7.4    then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
     7.5  qed
     7.6  
     7.7 -subsection\<open>Jeremy Avigad's @{text"More_Group"} material\<close>
     7.8 +subsection\<open>Jeremy Avigad's \<open>More_Group\<close> material\<close>
     7.9  
    7.10  text \<open>
    7.11    Show that the units in any monoid give rise to a group.
     8.1 --- a/src/HOL/Algebra/Ring.thy	Thu Nov 08 22:02:07 2018 +0100
     8.2 +++ b/src/HOL/Algebra/Ring.thy	Thu Nov 08 22:29:09 2018 +0100
     8.3 @@ -807,7 +807,7 @@
     8.4    "\<lbrakk> f \<in> ring_hom R S; g \<in> ring_hom S T \<rbrakk> \<Longrightarrow> g \<circ> f \<in> ring_hom R T"
     8.5    by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one)
     8.6  
     8.7 -subsection\<open>Jeremy Avigad's @{text"More_Finite_Product"} material\<close>
     8.8 +subsection\<open>Jeremy Avigad's \<open>More_Finite_Product\<close> material\<close>
     8.9  
    8.10  (* need better simplification rules for rings *)
    8.11  (* the next one holds more generally for abelian groups *)
    8.12 @@ -857,7 +857,7 @@
    8.13    "finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a [^] card(Units R) = \<one>"
    8.14    by (metis comm_group.power_order_eq_one units_comm_group units_of_carrier units_of_one units_of_pow)
    8.15  
    8.16 -subsection\<open>Jeremy Avigad's @{text"More_Ring"} material\<close>
    8.17 +subsection\<open>Jeremy Avigad's \<open>More_Ring\<close> material\<close>
    8.18  
    8.19  lemma (in cring) field_intro2: 
    8.20    assumes "\<zero>\<^bsub>R\<^esub> \<noteq> \<one>\<^bsub>R\<^esub>" and un: "\<And>x. x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>} \<Longrightarrow> x \<in> Units R"
     9.1 --- a/src/HOL/Algebra/Sylow.thy	Thu Nov 08 22:02:07 2018 +0100
     9.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu Nov 08 22:29:09 2018 +0100
     9.3 @@ -8,7 +8,7 @@
     9.4  
     9.5  text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
     9.6  
     9.7 -text \<open>The combinatorial argument is in theory @{text "Exponent"}.\<close>
     9.8 +text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>
     9.9  
    9.10  lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
    9.11    for c :: nat
    10.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 08 22:02:07 2018 +0100
    10.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 08 22:29:09 2018 +0100
    10.3 @@ -229,7 +229,7 @@
    10.4  proof -
    10.5    obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
    10.6      using assms unfolding invertible_def by auto
    10.7 -  with `k \<noteq> 0`
    10.8 +  with \<open>k \<noteq> 0\<close>
    10.9    have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
   10.10      by (simp_all add: assms matrix_scalar_ac)
   10.11    thus "invertible (k *\<^sub>R A)"
    11.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 08 22:02:07 2018 +0100
    11.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 08 22:29:09 2018 +0100
    11.3 @@ -625,7 +625,7 @@
    11.4      by (simp add: measure_linear_image \<open>linear f\<close> S f)
    11.5  qed
    11.6  
    11.7 -subsection%important\<open>@{text F_sigma} and @{text G_delta} sets.\<close>(*FIX ME mv *)
    11.8 +subsection%important\<open>\<open>F_sigma\<close> and \<open>G_delta\<close> sets.\<close>(*FIX ME mv *)
    11.9  
   11.10  (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
   11.11  inductive%important fsigma :: "'a::topological_space set \<Rightarrow> bool" where
   11.12 @@ -689,7 +689,7 @@
   11.13  lemma%unimportant gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
   11.14    using fsigma_imp_gdelta gdelta_imp_fsigma by force
   11.15  
   11.16 -text\<open>A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\<close>
   11.17 +text\<open>A Lebesgue set is almost an \<open>F_sigma\<close> or \<open>G_delta\<close>.\<close>
   11.18  lemma%unimportant lebesgue_set_almost_fsigma:
   11.19    assumes "S \<in> sets lebesgue"
   11.20    obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T"
    12.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Nov 08 22:02:07 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Nov 08 22:29:09 2018 +0100
    12.3 @@ -1228,7 +1228,7 @@
    12.4  proof%unimportant -
    12.5    obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
    12.6      using assms unfolding invertible_def by auto
    12.7 -  with `k \<noteq> 0`
    12.8 +  with \<open>k \<noteq> 0\<close>
    12.9    have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
   12.10      by (simp_all add: assms matrix_scalar_ac)
   12.11    thus "invertible (k *\<^sub>R A)"
    13.1 --- a/src/HOL/Analysis/Starlike.thy	Thu Nov 08 22:02:07 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Nov 08 22:29:09 2018 +0100
    13.3 @@ -7957,7 +7957,7 @@
    13.4  qed
    13.5  
    13.6  
    13.7 -subsection{*Orthogonal complement*}
    13.8 +subsection\<open>Orthogonal complement\<close>
    13.9  
   13.10  definition orthogonal_comp ("_\<^sup>\<bottom>" [80] 80)
   13.11    where "orthogonal_comp W \<equiv> {x. \<forall>y \<in> W. orthogonal y x}"
    14.1 --- a/src/HOL/Eisbach/Eisbach.thy	Thu Nov 08 22:02:07 2018 +0100
    14.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Thu Nov 08 22:29:09 2018 +0100
    14.3 @@ -90,9 +90,9 @@
    14.4  \<close>
    14.5  
    14.6  
    14.7 -text \<open>The following @{text fails} and @{text succeeds} methods protect the goal from the effect
    14.8 +text \<open>The following \<open>fails\<close> and \<open>succeeds\<close> methods protect the goal from the effect
    14.9        of a method, instead simply determining whether or not it can be applied to the current goal.
   14.10 -      The @{text fails} method inverts success, only succeeding if the given method would fail.\<close>
   14.11 +      The \<open>fails\<close> method inverts success, only succeeding if the given method would fail.\<close>
   14.12  
   14.13  method_setup fails =
   14.14   \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    15.1 --- a/src/HOL/Filter.thy	Thu Nov 08 22:02:07 2018 +0100
    15.2 +++ b/src/HOL/Filter.thy	Thu Nov 08 22:29:09 2018 +0100
    15.3 @@ -1208,7 +1208,7 @@
    15.4  
    15.5    show "(\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j) \<le> (\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j)"
    15.6      by (fast intro: le_prod_filterI INF_greatest INF_lower2
    15.7 -      order_trans[OF filtermap_INF] `i \<in> I` `j \<in> J`
    15.8 +      order_trans[OF filtermap_INF] \<open>i \<in> I\<close> \<open>j \<in> J\<close>
    15.9        filtermap_fst_prod_filter filtermap_snd_prod_filter)
   15.10    show "(\<Sqinter>i\<in>I. A i) \<times>\<^sub>F (\<Sqinter>j\<in>J. B j) \<le> (\<Sqinter>i\<in>I. \<Sqinter>j\<in>J. A i \<times>\<^sub>F B j)"
   15.11      by (intro INF_greatest prod_filter_mono INF_lower)
    16.1 --- a/src/HOL/Library/Code_Lazy.thy	Thu Nov 08 22:02:07 2018 +0100
    16.2 +++ b/src/HOL/Library/Code_Lazy.thy	Thu Nov 08 22:29:09 2018 +0100
    16.3 @@ -39,7 +39,7 @@
    16.4  
    16.5  ML_file "case_converter.ML"
    16.6  
    16.7 -subsection \<open>The type @{text lazy}\<close>
    16.8 +subsection \<open>The type \<open>lazy\<close>\<close>
    16.9  
   16.10  typedef 'a lazy = "UNIV :: 'a set" ..
   16.11  setup_lifting type_definition_lazy
    17.1 --- a/src/HOL/Library/IArray.thy	Thu Nov 08 22:02:07 2018 +0100
    17.2 +++ b/src/HOL/Library/IArray.thy	Thu Nov 08 22:29:09 2018 +0100
    17.3 @@ -188,9 +188,9 @@
    17.4  
    17.5  subsection \<open>Code Generation for Haskell\<close>
    17.6  
    17.7 -text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to @{text Data.Array.IArray.array}
    17.8 -  in Haskell.  Performance mapping to @{text Data.Array.Unboxed.Array} and
    17.9 -  @{text Data.Array.Array} is similar.\<close>
   17.10 +text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to \<open>Data.Array.IArray.array\<close>
   17.11 +  in Haskell.  Performance mapping to \<open>Data.Array.Unboxed.Array\<close> and
   17.12 +  \<open>Data.Array.Array\<close> is similar.\<close>
   17.13  
   17.14  code_printing
   17.15    code_module "IArray" \<rightharpoonup> (Haskell) \<open>
    18.1 --- a/src/HOL/Library/Landau_Symbols.thy	Thu Nov 08 22:02:07 2018 +0100
    18.2 +++ b/src/HOL/Library/Landau_Symbols.thy	Thu Nov 08 22:29:09 2018 +0100
    18.3 @@ -4,7 +4,7 @@
    18.4  
    18.5    Landau symbols for reasoning about the asymptotic growth of functions. 
    18.6  *)
    18.7 -section {* Definition of Landau symbols *}
    18.8 +section \<open>Definition of Landau symbols\<close>
    18.9  
   18.10  theory Landau_Symbols
   18.11  imports 
   18.12 @@ -16,14 +16,14 @@
   18.13    by (rule eventually_subst, erule eventually_rev_mp) simp
   18.14  
   18.15  
   18.16 -subsection {* Definition of Landau symbols *}
   18.17 +subsection \<open>Definition of Landau symbols\<close>
   18.18  
   18.19 -text {*
   18.20 +text \<open>
   18.21    Our Landau symbols are sign-oblivious, i.e. any function always has the same growth 
   18.22    as its absolute. This has the advantage of making some cancelling rules for sums nicer, but 
   18.23    introduces some problems in other places. Nevertheless, we found this definition more convenient
   18.24    to work with.
   18.25 -*}
   18.26 +\<close>
   18.27  
   18.28  definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set" 
   18.29      ("(1O[_]'(_'))")
   18.30 @@ -61,7 +61,7 @@
   18.31    "\<Theta>(g) \<equiv> bigtheta at_top g"
   18.32      
   18.33  
   18.34 -text {* The following is a set of properties that all Landau symbols satisfy. *}
   18.35 +text \<open>The following is a set of properties that all Landau symbols satisfy.\<close>
   18.36  
   18.37  named_theorems landau_divide_simps
   18.38  
   18.39 @@ -290,11 +290,11 @@
   18.40  end
   18.41  
   18.42  
   18.43 -text {* 
   18.44 +text \<open>
   18.45    The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with 
   18.46    $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
   18.47    The following locale captures this fact.
   18.48 -*}
   18.49 +\<close>
   18.50  
   18.51  locale landau_pair = 
   18.52    fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
   18.53 @@ -606,12 +606,12 @@
   18.54    } note A = this
   18.55    {
   18.56      fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   18.57 -    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   18.58 +    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   18.59        show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
   18.60    }
   18.61    {
   18.62      fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
   18.63 -    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   18.64 +    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   18.65        have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
   18.66      thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
   18.67    }
   18.68 @@ -689,13 +689,13 @@
   18.69    } note A = this
   18.70    {
   18.71      fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   18.72 -    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   18.73 +    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"] 
   18.74        show "l F (\<lambda>x. c * f x) = l F f" 
   18.75          by (intro equalityI small_subsetI) (simp_all add: field_simps)
   18.76    }
   18.77    {
   18.78      fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
   18.79 -    from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   18.80 +    from \<open>c \<noteq> 0\<close> and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
   18.81        have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
   18.82      thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
   18.83    }
   18.84 @@ -763,7 +763,7 @@
   18.85  qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
   18.86  
   18.87  
   18.88 -text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
   18.89 +text \<open>These rules allow chaining of Landau symbol propositions in Isar with "also".\<close>
   18.90  
   18.91  lemma big_mult_1:    "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
   18.92    and big_mult_1':   "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
   18.93 @@ -1028,7 +1028,7 @@
   18.94  qed
   18.95  
   18.96  
   18.97 -subsection {* Landau symbols and limits *}
   18.98 +subsection \<open>Landau symbols and limits\<close>
   18.99  
  18.100  lemma bigoI_tendsto_norm:
  18.101    fixes f g
  18.102 @@ -1073,7 +1073,7 @@
  18.103      with c_not_0 show "c/2 > 0" by simp
  18.104      from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
  18.105        by (subst (asm) tendsto_iff) (simp add: dist_real_def)
  18.106 -    from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
  18.107 +    from ev[OF \<open>c/2 > 0\<close>] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
  18.108      proof (eventually_elim)
  18.109        fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
  18.110        from B have g: "g x \<noteq> 0" by auto
  18.111 @@ -1523,16 +1523,16 @@
  18.112      assume "p < q"
  18.113      hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  18.114        by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  18.115 -    with `p < q` show ?thesis by auto
  18.116 +    with \<open>p < q\<close> show ?thesis by auto
  18.117    next
  18.118      assume "p = q"
  18.119      hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  18.120 -    with B `p = q` show ?thesis by auto
  18.121 +    with B \<open>p = q\<close> show ?thesis by auto
  18.122    next
  18.123      assume "p > q"
  18.124      hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
  18.125        by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
  18.126 -    with B `p > q` show ?thesis by auto
  18.127 +    with B \<open>p > q\<close> show ?thesis by auto
  18.128    qed
  18.129  qed
  18.130  
  18.131 @@ -1554,16 +1554,16 @@
  18.132      assume "p < q"
  18.133      hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
  18.134        by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  18.135 -    with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
  18.136 +    with \<open>p < q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
  18.137    next
  18.138      assume "p = q"
  18.139      hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
  18.140 -    with B `p = q` show ?thesis by auto
  18.141 +    with B \<open>p = q\<close> show ?thesis by auto
  18.142    next
  18.143      assume "p > q"
  18.144      hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
  18.145        by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
  18.146 -    with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
  18.147 +    with B \<open>p > q\<close> show ?thesis by (auto intro: landau_o.small_imp_big)
  18.148    qed
  18.149  qed
  18.150  
    19.1 --- a/src/HOL/Limits.thy	Thu Nov 08 22:02:07 2018 +0100
    19.2 +++ b/src/HOL/Limits.thy	Thu Nov 08 22:29:09 2018 +0100
    19.3 @@ -173,7 +173,7 @@
    19.4      unfolding Bfun_def by fast
    19.5    with assms(1) have "eventually (\<lambda>n. norm (f n) \<le> K) sequentially"
    19.6      by (fast elim: eventually_elim2 order_trans)
    19.7 -  with `0 < K` show "Bseq f"
    19.8 +  with \<open>0 < K\<close> show "Bseq f"
    19.9      unfolding Bfun_def by fast
   19.10  qed
   19.11  
    20.1 --- a/src/HOL/ROOT	Thu Nov 08 22:02:07 2018 +0100
    20.2 +++ b/src/HOL/ROOT	Thu Nov 08 22:29:09 2018 +0100
    20.3 @@ -1,9 +1,9 @@
    20.4  chapter HOL
    20.5  
    20.6  session HOL (main) = Pure +
    20.7 -  description {*
    20.8 +  description \<open>
    20.9      Classical Higher-order Logic.
   20.10 -  *}
   20.11 +\<close>
   20.12    options [strict_facts]
   20.13    theories
   20.14      Main (global)
   20.15 @@ -13,9 +13,9 @@
   20.16      "root.tex"
   20.17  
   20.18  session "HOL-Proofs" (timing) = Pure +
   20.19 -  description {*
   20.20 +  description \<open>
   20.21      HOL-Main with explicit proof terms.
   20.22 -  *}
   20.23 +\<close>
   20.24    options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0, parallel_limit = 500]
   20.25    sessions
   20.26      "HOL-Library"
   20.27 @@ -23,9 +23,9 @@
   20.28      "HOL-Library.Realizers"
   20.29  
   20.30  session "HOL-Library" (main timing) in Library = HOL +
   20.31 -  description {*
   20.32 +  description \<open>
   20.33      Classical Higher-order Logic -- batteries included.
   20.34 -  *}
   20.35 +\<close>
   20.36    theories
   20.37      Library
   20.38      (*conflicting type class instantiations and dependent applications*)
   20.39 @@ -100,7 +100,7 @@
   20.40      "style.sty"
   20.41  
   20.42  session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
   20.43 -  description {*
   20.44 +  description \<open>
   20.45      Author:     Gertrud Bauer, TU Munich
   20.46  
   20.47      The Hahn-Banach theorem for real vector spaces.
   20.48 @@ -116,7 +116,7 @@
   20.49      The theorem says, that every continous linearform, defined on arbitrary
   20.50      subspaces (not only one-dimensional subspaces), can be extended to a
   20.51      continous linearform on the whole vectorspace.
   20.52 -  *}
   20.53 +\<close>
   20.54    sessions
   20.55      "HOL-Analysis"
   20.56    theories
   20.57 @@ -124,7 +124,7 @@
   20.58    document_files "root.bib" "root.tex"
   20.59  
   20.60  session "HOL-Induct" in Induct = "HOL-Library" +
   20.61 -  description {*
   20.62 +  description \<open>
   20.63      Examples of (Co)Inductive Definitions.
   20.64  
   20.65      Comb proves the Church-Rosser theorem for combinators (see
   20.66 @@ -139,7 +139,7 @@
   20.67  
   20.68      Exp demonstrates the use of iterated inductive definitions to reason about
   20.69      mutually recursive relations.
   20.70 -  *}
   20.71 +\<close>
   20.72    theories [quick_and_dirty]
   20.73      Common_Patterns
   20.74    theories
   20.75 @@ -193,7 +193,7 @@
   20.76    document_files "root.bib" "root.tex"
   20.77  
   20.78  session "HOL-IMPP" in IMPP = HOL +
   20.79 -  description {*
   20.80 +  description \<open>
   20.81      Author:     David von Oheimb
   20.82      Copyright   1999 TUM
   20.83  
   20.84 @@ -202,7 +202,7 @@
   20.85      This is an extension of IMP with local variables and mutually recursive
   20.86      procedures. For documentation see "Hoare Logic for Mutual Recursion and
   20.87      Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   20.88 -  *}
   20.89 +\<close>
   20.90    theories EvenOdd
   20.91  
   20.92  session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   20.93 @@ -233,10 +233,10 @@
   20.94    theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   20.95  
   20.96  session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
   20.97 -  description {*
   20.98 +  description \<open>
   20.99      Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
  20.100      Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
  20.101 -  *}
  20.102 +\<close>
  20.103    sessions
  20.104      "HOL-Algebra"
  20.105    theories
  20.106 @@ -245,18 +245,18 @@
  20.107      "root.tex"
  20.108  
  20.109  session "HOL-Hoare" in Hoare = HOL +
  20.110 -  description {*
  20.111 +  description \<open>
  20.112      Verification of imperative programs (verification conditions are generated
  20.113      automatically from pre/post conditions and loop invariants).
  20.114 -  *}
  20.115 +\<close>
  20.116    theories Hoare
  20.117    document_files "root.bib" "root.tex"
  20.118  
  20.119  session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
  20.120 -  description {*
  20.121 +  description \<open>
  20.122      Verification of shared-variable imperative programs a la Owicki-Gries.
  20.123      (verification conditions are generated automatically).
  20.124 -  *}
  20.125 +\<close>
  20.126    theories Hoare_Parallel
  20.127    document_files "root.bib" "root.tex"
  20.128  
  20.129 @@ -282,12 +282,12 @@
  20.130      Code_Test_SMLNJ
  20.131  
  20.132  session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
  20.133 -  description {*
  20.134 +  description \<open>
  20.135      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
  20.136      Author:     Jasmin Blanchette, TU Muenchen
  20.137  
  20.138      Testing Metis and Sledgehammer.
  20.139 -  *}
  20.140 +\<close>
  20.141    sessions
  20.142      "HOL-Decision_Procs"
  20.143    theories
  20.144 @@ -302,18 +302,18 @@
  20.145      Sets
  20.146  
  20.147  session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
  20.148 -  description {*
  20.149 +  description \<open>
  20.150      Author:     Jasmin Blanchette, TU Muenchen
  20.151      Copyright   2009
  20.152 -  *}
  20.153 +\<close>
  20.154    theories [quick_and_dirty] Nitpick_Examples
  20.155  
  20.156  session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
  20.157 -  description {*
  20.158 +  description \<open>
  20.159      Author: Clemens Ballarin, started 24 September 1999, and many others
  20.160  
  20.161      The Isabelle Algebraic Library.
  20.162 -  *}
  20.163 +\<close>
  20.164    theories
  20.165      (* Orders and Lattices *)
  20.166      Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
  20.167 @@ -332,9 +332,9 @@
  20.168    document_files "root.bib" "root.tex"
  20.169  
  20.170  session "HOL-Auth" (timing) in Auth = "HOL-Library" +
  20.171 -  description {*
  20.172 +  description \<open>
  20.173      A new approach to verifying authentication protocols.
  20.174 -  *}
  20.175 +\<close>
  20.176    theories
  20.177      Auth_Shared
  20.178      Auth_Public
  20.179 @@ -344,12 +344,12 @@
  20.180    document_files "root.tex"
  20.181  
  20.182  session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
  20.183 -  description {*
  20.184 +  description \<open>
  20.185      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
  20.186      Copyright   1998  University of Cambridge
  20.187  
  20.188      Verifying security protocols using Chandy and Misra's UNITY formalism.
  20.189 -  *}
  20.190 +\<close>
  20.191    theories
  20.192      (*Basic meta-theory*)
  20.193      UNITY_Main
  20.194 @@ -404,9 +404,9 @@
  20.195    document_files "root.bib" "root.tex"
  20.196  
  20.197  session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
  20.198 -  description {*
  20.199 +  description \<open>
  20.200      Various decision procedures, typically involving reflection.
  20.201 -  *}
  20.202 +\<close>
  20.203    theories
  20.204      Decision_Procs
  20.205  
  20.206 @@ -419,9 +419,9 @@
  20.207      XML_Data
  20.208  
  20.209  session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
  20.210 -  description {*
  20.211 +  description \<open>
  20.212      Examples for program extraction in Higher-Order Logic.
  20.213 -  *}
  20.214 +\<close>
  20.215    options [parallel_proofs = 0, quick_and_dirty = false]
  20.216    sessions
  20.217      "HOL-Computational_Algebra"
  20.218 @@ -434,7 +434,7 @@
  20.219    document_files "root.bib" "root.tex"
  20.220  
  20.221  session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
  20.222 -  description {*
  20.223 +  description \<open>
  20.224      Lambda Calculus in de Bruijn's Notation.
  20.225  
  20.226      This session defines lambda-calculus terms with de Bruijn indixes and
  20.227 @@ -442,7 +442,7 @@
  20.228  
  20.229      The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
  20.230      theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
  20.231 -  *}
  20.232 +\<close>
  20.233    options [print_mode = "no_brackets",
  20.234      parallel_proofs = 0, quick_and_dirty = false]
  20.235    sessions
  20.236 @@ -455,7 +455,7 @@
  20.237    document_files "root.bib" "root.tex"
  20.238  
  20.239  session "HOL-Prolog" in Prolog = HOL +
  20.240 -  description {*
  20.241 +  description \<open>
  20.242      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
  20.243  
  20.244      A bare-bones implementation of Lambda-Prolog.
  20.245 @@ -463,15 +463,15 @@
  20.246      This is a simple exploratory implementation of Lambda-Prolog in HOL,
  20.247      including some minimal examples (in Test.thy) and a more typical example of
  20.248      a little functional language and its type system.
  20.249 -  *}
  20.250 +\<close>
  20.251    theories Test Type
  20.252  
  20.253  session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" +
  20.254 -  description {*
  20.255 +  description \<open>
  20.256      Formalization of a fragment of Java, together with a corresponding virtual
  20.257      machine and a specification of its bytecode verifier and a lightweight
  20.258      bytecode verifier, including proofs of type-safety.
  20.259 -  *}
  20.260 +\<close>
  20.261    sessions
  20.262      "HOL-Eisbach"
  20.263    theories
  20.264 @@ -482,9 +482,9 @@
  20.265      "root.tex"
  20.266  
  20.267  session "HOL-NanoJava" in NanoJava = HOL +
  20.268 -  description {*
  20.269 +  description \<open>
  20.270      Hoare Logic for a tiny fragment of Java.
  20.271 -  *}
  20.272 +\<close>
  20.273    theories Example
  20.274    document_files "root.bib" "root.tex"
  20.275  
  20.276 @@ -498,7 +498,7 @@
  20.277    document_files "root.tex"
  20.278  
  20.279  session "HOL-IOA" in IOA = HOL +
  20.280 -  description {*
  20.281 +  description \<open>
  20.282      Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
  20.283      Copyright   1994--1996  TU Muenchen
  20.284  
  20.285 @@ -524,22 +524,22 @@
  20.286      organization={Aarhus University, BRICS report},
  20.287      year=1995}
  20.288      ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
  20.289 -  *}
  20.290 +\<close>
  20.291    theories Solve
  20.292  
  20.293  session "HOL-Lattice" in Lattice = HOL +
  20.294 -  description {*
  20.295 +  description \<open>
  20.296      Author:     Markus Wenzel, TU Muenchen
  20.297  
  20.298      Basic theory of lattices and orders.
  20.299 -  *}
  20.300 +\<close>
  20.301    theories CompleteLattice
  20.302    document_files "root.tex"
  20.303  
  20.304  session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
  20.305 -  description {*
  20.306 +  description \<open>
  20.307      Miscellaneous examples for Higher-Order Logic.
  20.308 -  *}
  20.309 +\<close>
  20.310    theories
  20.311      Adhoc_Overloading_Examples
  20.312      Antiquote
  20.313 @@ -634,9 +634,9 @@
  20.314      Meson_Test
  20.315  
  20.316  session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
  20.317 -  description {*
  20.318 +  description \<open>
  20.319      Miscellaneous Isabelle/Isar examples.
  20.320 -  *}
  20.321 +\<close>
  20.322    options [quick_and_dirty]
  20.323    theories
  20.324      Knaster_Tarski
  20.325 @@ -661,9 +661,9 @@
  20.326      "root.tex"
  20.327  
  20.328  session "HOL-Eisbach" in Eisbach = HOL +
  20.329 -  description {*
  20.330 +  description \<open>
  20.331      The Eisbach proof method language and "match" method.
  20.332 -  *}
  20.333 +\<close>
  20.334    sessions
  20.335      FOL
  20.336    theories
  20.337 @@ -673,24 +673,24 @@
  20.338      Examples_FOL
  20.339  
  20.340  session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" +
  20.341 -  description {*
  20.342 +  description \<open>
  20.343      Verification of the SET Protocol.
  20.344 -  *}
  20.345 +\<close>
  20.346    theories
  20.347      SET_Protocol
  20.348    document_files "root.tex"
  20.349  
  20.350  session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
  20.351 -  description {*
  20.352 +  description \<open>
  20.353      Two-dimensional matrices and linear programming.
  20.354 -  *}
  20.355 +\<close>
  20.356    theories Cplex
  20.357    document_files "root.tex"
  20.358  
  20.359  session "HOL-TLA" in TLA = HOL +
  20.360 -  description {*
  20.361 +  description \<open>
  20.362      Lamport's Temporal Logic of Actions.
  20.363 -  *}
  20.364 +\<close>
  20.365    theories TLA
  20.366  
  20.367  session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
  20.368 @@ -703,13 +703,13 @@
  20.369    theories MemoryImplementation
  20.370  
  20.371  session "HOL-TPTP" in TPTP = "HOL-Library" +
  20.372 -  description {*
  20.373 +  description \<open>
  20.374      Author:     Jasmin Blanchette, TU Muenchen
  20.375      Author:     Nik Sultana, University of Cambridge
  20.376      Copyright   2011
  20.377  
  20.378      TPTP-related extensions.
  20.379 -  *}
  20.380 +\<close>
  20.381    theories
  20.382      ATP_Theory_Export
  20.383      MaSh_Eval
  20.384 @@ -760,9 +760,9 @@
  20.385      VC_Condition
  20.386  
  20.387  session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
  20.388 -  description {*
  20.389 +  description \<open>
  20.390      Ordinals and Cardinals, Full Theories.
  20.391 -  *}
  20.392 +\<close>
  20.393    theories
  20.394      Cardinals
  20.395      Bounded_Set
  20.396 @@ -772,9 +772,9 @@
  20.397      "root.bib"
  20.398  
  20.399  session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
  20.400 -  description {*
  20.401 +  description \<open>
  20.402      (Co)datatype Examples.
  20.403 -  *}
  20.404 +\<close>
  20.405    theories
  20.406      Compat
  20.407      Lambda_Term
  20.408 @@ -792,9 +792,9 @@
  20.409      Misc_Primrec
  20.410  
  20.411  session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
  20.412 -  description {*
  20.413 +  description \<open>
  20.414      Corecursion Examples.
  20.415 -  *}
  20.416 +\<close>
  20.417    theories
  20.418      LFilter
  20.419      Paper_Examples
  20.420 @@ -828,9 +828,9 @@
  20.421    document_files "root.tex"
  20.422  
  20.423  session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
  20.424 -  description {*
  20.425 +  description \<open>
  20.426      Nonstandard analysis.
  20.427 -  *}
  20.428 +\<close>
  20.429    theories
  20.430      Nonstandard_Analysis
  20.431    document_files "root.tex"
  20.432 @@ -911,9 +911,9 @@
  20.433      Quickcheck_Narrowing_Examples
  20.434  
  20.435  session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
  20.436 -  description {*
  20.437 +  description \<open>
  20.438      Author:     Cezary Kaliszyk and Christian Urban
  20.439 -  *}
  20.440 +\<close>
  20.441    theories
  20.442      DList
  20.443      Quotient_FSet
  20.444 @@ -949,9 +949,9 @@
  20.445      Reg_Exp_Example
  20.446  
  20.447  session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
  20.448 -  description {*
  20.449 +  description \<open>
  20.450      Experimental extension of Higher-Order Logic to allow translation of types to sets.
  20.451 -  *}
  20.452 +\<close>
  20.453    theories
  20.454      Types_To_Sets
  20.455      "Examples/Prerequisites"
  20.456 @@ -960,12 +960,12 @@
  20.457      "Examples/Linear_Algebra_On"
  20.458  
  20.459  session HOLCF (main timing) in HOLCF = HOL +
  20.460 -  description {*
  20.461 +  description \<open>
  20.462      Author:     Franz Regensburger
  20.463      Author:     Brian Huffman
  20.464  
  20.465      HOLCF -- a semantic extension of HOL by the LCF logic.
  20.466 -  *}
  20.467 +\<close>
  20.468    sessions
  20.469      "HOL-Library"
  20.470    theories
  20.471 @@ -985,11 +985,11 @@
  20.472      HOL_Cpo
  20.473  
  20.474  session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
  20.475 -  description {*
  20.476 +  description \<open>
  20.477      IMP -- A WHILE-language and its Semantics.
  20.478  
  20.479      This is the HOLCF-based denotational semantics of a simple WHILE-language.
  20.480 -  *}
  20.481 +\<close>
  20.482    sessions
  20.483      "HOL-IMP"
  20.484    theories
  20.485 @@ -1000,9 +1000,9 @@
  20.486      "root.bib"
  20.487  
  20.488  session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
  20.489 -  description {*
  20.490 +  description \<open>
  20.491      Miscellaneous examples for HOLCF.
  20.492 -  *}
  20.493 +\<close>
  20.494    theories
  20.495      Dnat
  20.496      Dagstuhl
  20.497 @@ -1017,7 +1017,7 @@
  20.498      Pattern_Match
  20.499  
  20.500  session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
  20.501 -  description {*
  20.502 +  description \<open>
  20.503      FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  20.504  
  20.505      For introductions to FOCUS, see
  20.506 @@ -1030,14 +1030,14 @@
  20.507  
  20.508      "Specification and Development of Interactive Systems: Focus on Streams,
  20.509      Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  20.510 -  *}
  20.511 +\<close>
  20.512    theories
  20.513      Fstreams
  20.514      FOCUS
  20.515      Buffer_adm
  20.516  
  20.517  session IOA (timing) in "HOLCF/IOA" = HOLCF +
  20.518 -  description {*
  20.519 +  description \<open>
  20.520      Author:     Olaf Mueller
  20.521      Copyright   1997 TU München
  20.522  
  20.523 @@ -1046,40 +1046,40 @@
  20.524      The distribution contains simulation relations, temporal logic, and an
  20.525      abstraction theory. Everything is based upon a domain-theoretic model of
  20.526      finite and infinite sequences.
  20.527 -  *}
  20.528 +\<close>
  20.529    theories Abstraction
  20.530  
  20.531  session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  20.532 -  description {*
  20.533 +  description \<open>
  20.534      Author:     Olaf Mueller
  20.535  
  20.536      The Alternating Bit Protocol performed in I/O-Automata.
  20.537 -  *}
  20.538 +\<close>
  20.539    theories
  20.540      Correctness
  20.541      Spec
  20.542  
  20.543  session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  20.544 -  description {*
  20.545 +  description \<open>
  20.546      Author:     Tobias Nipkow & Konrad Slind
  20.547  
  20.548      A network transmission protocol, performed in the
  20.549      I/O automata formalization by Olaf Mueller.
  20.550 -  *}
  20.551 +\<close>
  20.552    theories Correctness
  20.553  
  20.554  session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  20.555 -  description {*
  20.556 +  description \<open>
  20.557      Author:     Olaf Mueller
  20.558  
  20.559      Memory storage case study.
  20.560 -  *}
  20.561 +\<close>
  20.562    theories Correctness
  20.563  
  20.564  session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  20.565 -  description {*
  20.566 +  description \<open>
  20.567      Author:     Olaf Mueller
  20.568 -  *}
  20.569 +\<close>
  20.570    theories
  20.571      TrivEx
  20.572      TrivEx2
    21.1 --- a/src/HOL/String.thy	Thu Nov 08 22:02:07 2018 +0100
    21.2 +++ b/src/HOL/String.thy	Thu Nov 08 22:29:09 2018 +0100
    21.3 @@ -398,16 +398,16 @@
    21.4  text \<open>
    21.5    Logical ground representations for literals are:
    21.6  
    21.7 -  \<^enum> @{text 0} for the empty literal;
    21.8 +  \<^enum> \<open>0\<close> for the empty literal;
    21.9  
   21.10 -  \<^enum> @{text "Literal b0 \<dots> b6 s"} for a literal starting with one
   21.11 +  \<^enum> \<open>Literal b0 \<dots> b6 s\<close> for a literal starting with one
   21.12      character and continued by another literal.
   21.13  
   21.14    Syntactic representations for literals are:
   21.15  
   21.16 -  \<^enum> Printable text as string prefixed with @{text STR};
   21.17 +  \<^enum> Printable text as string prefixed with \<open>STR\<close>;
   21.18  
   21.19 -  \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
   21.20 +  \<^enum> A single ascii value as numerical hexadecimal value prefixed with \<open>STR\<close>.
   21.21  \<close>
   21.22  
   21.23  instantiation String.literal :: zero
    22.1 --- a/src/HOL/Transcendental.thy	Thu Nov 08 22:02:07 2018 +0100
    22.2 +++ b/src/HOL/Transcendental.thy	Thu Nov 08 22:29:09 2018 +0100
    22.3 @@ -4009,7 +4009,7 @@
    22.4    shows "0 < sin (pi / real n)"
    22.5    by (rule sin_gt_zero) (use assms in \<open>simp_all add: divide_simps\<close>)
    22.6  
    22.7 -text\<open>Proof resembles that of @{text cos_is_zero} but with @{term pi} for the upper bound\<close>
    22.8 +text\<open>Proof resembles that of \<open>cos_is_zero\<close> but with @{term pi} for the upper bound\<close>
    22.9  lemma cos_total:
   22.10    assumes y: "-1 \<le> y" "y \<le> 1"
   22.11    shows "\<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = y"
    23.1 --- a/src/LCF/ROOT	Thu Nov 08 22:02:07 2018 +0100
    23.2 +++ b/src/LCF/ROOT	Thu Nov 08 22:29:09 2018 +0100
    23.3 @@ -1,7 +1,7 @@
    23.4  chapter LCF
    23.5  
    23.6  session LCF = Pure +
    23.7 -  description {*
    23.8 +  description \<open>
    23.9      Author:     Tobias Nipkow
   23.10      Copyright   1992  University of Cambridge
   23.11  
   23.12 @@ -9,7 +9,7 @@
   23.13  
   23.14      Useful references on LCF: Lawrence C. Paulson,
   23.15      Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
   23.16 -  *}
   23.17 +\<close>
   23.18    sessions
   23.19      FOL
   23.20    theories
    24.1 --- a/src/Pure/ROOT	Thu Nov 08 22:02:07 2018 +0100
    24.2 +++ b/src/Pure/ROOT	Thu Nov 08 22:29:09 2018 +0100
    24.3 @@ -1,9 +1,9 @@
    24.4  chapter Pure
    24.5  
    24.6  session Pure =
    24.7 -  description {*
    24.8 +  description \<open>
    24.9      The Pure logical framework
   24.10 -  *}
   24.11 +\<close>
   24.12    options [threads = 1, export_theory]
   24.13    theories
   24.14      Pure (global)
    25.1 --- a/src/Sequents/ROOT	Thu Nov 08 22:02:07 2018 +0100
    25.2 +++ b/src/Sequents/ROOT	Thu Nov 08 22:29:09 2018 +0100
    25.3 @@ -1,7 +1,7 @@
    25.4  chapter Sequents
    25.5  
    25.6  session Sequents = Pure +
    25.7 -  description {*
    25.8 +  description \<open>
    25.9      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   25.10      Copyright   1991  University of Cambridge
   25.11  
   25.12 @@ -36,7 +36,7 @@
   25.13  
   25.14      S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
   25.15      of Cambridge Computer Lab, 1995, ed L. Paulson)
   25.16 -  *}
   25.17 +\<close>
   25.18    theories
   25.19      LK
   25.20      ILL
    26.1 --- a/src/ZF/ROOT	Thu Nov 08 22:02:07 2018 +0100
    26.2 +++ b/src/ZF/ROOT	Thu Nov 08 22:29:09 2018 +0100
    26.3 @@ -1,7 +1,7 @@
    26.4  chapter ZF
    26.5  
    26.6  session ZF (main timing) = Pure +
    26.7 -  description {*
    26.8 +  description \<open>
    26.9      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   26.10      Copyright   1995  University of Cambridge
   26.11  
   26.12 @@ -41,7 +41,7 @@
   26.13  
   26.14      Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
   26.15      (North-Holland, 1980)
   26.16 -  *}
   26.17 +\<close>
   26.18    sessions
   26.19      FOL
   26.20    theories
   26.21 @@ -50,7 +50,7 @@
   26.22    document_files "root.tex"
   26.23  
   26.24  session "ZF-AC" in AC = ZF +
   26.25 -  description {*
   26.26 +  description \<open>
   26.27      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   26.28      Copyright   1995  University of Cambridge
   26.29  
   26.30 @@ -63,7 +63,7 @@
   26.31      http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
   26.32      "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
   26.33      development and ZF's theories of cardinals.
   26.34 -  *}
   26.35 +\<close>
   26.36    theories
   26.37      WO6_WO1
   26.38      WO1_WO7
   26.39 @@ -78,7 +78,7 @@
   26.40    document_files "root.tex" "root.bib"
   26.41  
   26.42  session "ZF-Coind" in Coind = ZF +
   26.43 -  description {*
   26.44 +  description \<open>
   26.45      Author:     Jacob Frost, Cambridge University Computer Laboratory
   26.46      Copyright   1995  University of Cambridge
   26.47  
   26.48 @@ -99,11 +99,11 @@
   26.49          Jacob Frost, A Case Study of Co_induction in Isabelle
   26.50          Report, Computer Lab, University of Cambridge (1995).
   26.51          http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
   26.52 -  *}
   26.53 +\<close>
   26.54    theories ECR
   26.55  
   26.56  session "ZF-Constructible" in Constructible = ZF +
   26.57 -  description {*
   26.58 +  description \<open>
   26.59      Relative Consistency of the Axiom of Choice:
   26.60      Inner Models, Absoluteness and Consistency Proofs.
   26.61  
   26.62 @@ -121,7 +121,7 @@
   26.63  
   26.64      A paper describing this development is
   26.65      http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
   26.66 -  *}
   26.67 +\<close>
   26.68    theories
   26.69      DPow_absolute
   26.70      AC_in_L
   26.71 @@ -129,7 +129,7 @@
   26.72    document_files "root.tex" "root.bib"
   26.73  
   26.74  session "ZF-IMP" in IMP = ZF +
   26.75 -  description {*
   26.76 +  description \<open>
   26.77      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
   26.78      Copyright   1994 TUM
   26.79  
   26.80 @@ -141,19 +141,19 @@
   26.81  
   26.82      Glynn Winskel. The Formal Semantics of Programming Languages.
   26.83      MIT Press, 1993.
   26.84 -  *}
   26.85 +\<close>
   26.86    theories Equiv
   26.87    document_files
   26.88      "root.tex"
   26.89      "root.bib"
   26.90  
   26.91  session "ZF-Induct" in Induct = ZF +
   26.92 -  description {*
   26.93 +  description \<open>
   26.94      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   26.95      Copyright   2001  University of Cambridge
   26.96  
   26.97      Inductive definitions.
   26.98 -  *}
   26.99 +\<close>
  26.100    theories
  26.101      (** Datatypes **)
  26.102      Datatypes       (*sample datatypes*)
  26.103 @@ -181,7 +181,7 @@
  26.104      "root.tex"
  26.105  
  26.106  session "ZF-Resid" in Resid = ZF +
  26.107 -  description {*
  26.108 +  description \<open>
  26.109      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
  26.110      Copyright   1995  University of Cambridge
  26.111  
  26.112 @@ -196,16 +196,16 @@
  26.113      See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
  26.114      Porting Experiment.
  26.115      http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
  26.116 -  *}
  26.117 +\<close>
  26.118    theories Confluence
  26.119  
  26.120  session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
  26.121 -  description {*
  26.122 +  description \<open>
  26.123      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
  26.124      Copyright   1998  University of Cambridge
  26.125  
  26.126      ZF/UNITY proofs.
  26.127 -  *}
  26.128 +\<close>
  26.129    theories
  26.130      (*Simple examples: no composition*)
  26.131      Mutex
  26.132 @@ -217,7 +217,7 @@
  26.133      Distributor Merge ClientImpl AllocImpl
  26.134  
  26.135  session "ZF-ex" in ex = ZF +
  26.136 -  description {*
  26.137 +  description \<open>
  26.138      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
  26.139      Copyright   1993  University of Cambridge
  26.140  
  26.141 @@ -231,7 +231,7 @@
  26.142      describes the theoretical foundations of datatypes while
  26.143      href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
  26.144      describes the package that automates their declaration.
  26.145 -  *}
  26.146 +\<close>
  26.147    theories
  26.148      misc
  26.149      Ring             (*abstract algebra*)