clarified document antiquotation @{theory};
authorwenzelm
Fri Jun 22 20:31:49 2018 +0200 (14 months ago)
changeset 6848459793df7f853
parent 68483 087d32a40129
child 68485 28f9e9b80c49
clarified document antiquotation @{theory};
NEWS
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Foundations.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Refinement.thy
src/Doc/Datatypes/Datatypes.thy
src/Doc/Eisbach/Manual.thy
src/Doc/Eisbach/Preface.thy
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Main/Main_Doc.thy
src/Doc/Tutorial/Types/Axioms.thy
src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Data_Structures/Set2_Join.thy
src/HOL/Groebner_Basis.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Compiler2.thy
src/HOL/IMP/Live_True.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/RBT_Mapping.thy
src/HOL/Library/Tree_Multiset.thy
src/HOL/Library/Tree_Real.thy
src/HOL/Order_Relation.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Real.thy
src/HOL/ex/Erdoes_Szekeres.thy
src/HOL/ex/Sum_of_Powers.thy
src/Pure/Thy/document_antiquotations.ML
src/Pure/theory.ML
     1.1 --- a/NEWS	Fri Jun 22 18:31:50 2018 +0200
     1.2 +++ b/NEWS	Fri Jun 22 20:31:49 2018 +0200
     1.3 @@ -167,6 +167,10 @@
     1.4  * Document preparation with skip_proofs option now preserves the content
     1.5  more accurately: only terminal proof steps ('by' etc.) are skipped.
     1.6  
     1.7 +* Document antiquotation @{theory name} requires the long
     1.8 +session-qualified theory name: this is what users reading the text
     1.9 +normally need to import.
    1.10 +
    1.11  * Document antiquotation @{session name} checks and prints the given
    1.12  session name verbatim.
    1.13  
     2.1 --- a/src/Doc/Codegen/Adaptation.thy	Fri Jun 22 18:31:50 2018 +0200
     2.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Jun 22 20:31:49 2018 +0200
     2.3 @@ -151,7 +151,7 @@
     2.4  subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close>
     2.5  
     2.6  text \<open>
     2.7 -  The @{theory HOL} @{theory Main} theory already provides a code
     2.8 +  The @{theory Main} theory of Isabelle/HOL already provides a code
     2.9    generator setup which should be suitable for most applications.
    2.10    Common extensions and modifications are available by certain
    2.11    theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
    2.12 @@ -160,7 +160,7 @@
    2.13  
    2.14    \begin{description}
    2.15  
    2.16 -    \item[@{theory "Code_Numeral"}] provides additional numeric
    2.17 +    \item[@{theory "HOL.Code_Numeral"}] provides additional numeric
    2.18         types @{typ integer} and @{typ natural} isomorphic to types
    2.19         @{typ int} and @{typ nat} respectively.  Type @{typ integer}
    2.20         is mapped to target-language built-in integers; @{typ natural}
    2.21 @@ -168,7 +168,7 @@
    2.22         Useful for code setups which involve e.g.~indexing
    2.23         of target-language arrays.  Part of @{text "HOL-Main"}.
    2.24  
    2.25 -    \item[@{theory "String"}] provides an additional datatype @{typ
    2.26 +    \item[@{theory "HOL.String"}] provides an additional datatype @{typ
    2.27         String.literal} which is isomorphic to lists of 7-bit (ASCII) characters;
    2.28         @{typ String.literal}s are mapped to target-language strings.
    2.29  
    2.30 @@ -215,7 +215,7 @@
    2.31         containing both @{text "Code_Target_Nat"} and
    2.32         @{text "Code_Target_Int"}.
    2.33  
    2.34 -    \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
    2.35 +    \item[@{theory "HOL-Library.IArray"}] provides a type @{typ "'a iarray"}
    2.36         isomorphic to lists but implemented by (effectively immutable)
    2.37         arrays \emph{in SML only}.
    2.38  
     3.1 --- a/src/Doc/Codegen/Foundations.thy	Fri Jun 22 18:31:50 2018 +0200
     3.2 +++ b/src/Doc/Codegen/Foundations.thy	Fri Jun 22 20:31:49 2018 +0200
     3.3 @@ -11,9 +11,9 @@
     3.4    components which can be customised individually.
     3.5  
     3.6    Conceptually all components operate on Isabelle's logic framework
     3.7 -  @{theory Pure}.  Practically, the object logic @{theory HOL}
     3.8 +  Pure.  Practically, the object logic HOL
     3.9    provides the necessary facilities to make use of the code generator,
    3.10 -  mainly since it is an extension of @{theory Pure}.
    3.11 +  mainly since it is an extension of Isabelle/Pure.
    3.12  
    3.13    The constellation of the different components is visualized in the
    3.14    following picture.
     4.1 --- a/src/Doc/Codegen/Further.thy	Fri Jun 22 18:31:50 2018 +0200
     4.2 +++ b/src/Doc/Codegen/Further.thy	Fri Jun 22 20:31:49 2018 +0200
     4.3 @@ -30,7 +30,7 @@
     4.4    arbitrary ML code as well.
     4.5  
     4.6    A typical example for @{command code_reflect} can be found in the
     4.7 -  @{theory Predicate} theory.
     4.8 +  @{theory HOL.Predicate} theory.
     4.9  \<close>
    4.10  
    4.11  
     5.1 --- a/src/Doc/Codegen/Introduction.thy	Fri Jun 22 18:31:50 2018 +0200
     5.2 +++ b/src/Doc/Codegen/Introduction.thy	Fri Jun 22 20:31:49 2018 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4    @{cite "scala-overview-tech-report"}.
     5.5  
     5.6    To profit from this tutorial, some familiarity and experience with
     5.7 -  @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
     5.8 +  Isabelle/HOL @{cite "isa-tutorial"} and its basic theories is assumed.
     5.9  \<close>
    5.10  
    5.11  
     6.1 --- a/src/Doc/Codegen/Refinement.thy	Fri Jun 22 18:31:50 2018 +0200
     6.2 +++ b/src/Doc/Codegen/Refinement.thy	Fri Jun 22 20:31:49 2018 +0200
     6.3 @@ -188,7 +188,7 @@
     6.4    of distinct elements.
     6.5  
     6.6    The specification of @{typ "'a dlist"} itself can be found in theory
     6.7 -  @{theory Dlist}.
     6.8 +  @{theory "HOL-Library.Dlist"}.
     6.9  
    6.10    The first step is to decide on which representation the abstract
    6.11    type (in our example @{typ "'a dlist"}) should be implemented.
    6.12 @@ -271,9 +271,9 @@
    6.13    for the meta theory of datatype refinement involving invariants.
    6.14  
    6.15    Typical data structures implemented by representations involving
    6.16 -  invariants are available in the library, theory @{theory Mapping}
    6.17 +  invariants are available in the library, theory @{theory "HOL-Library.Mapping"}
    6.18    specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
    6.19 -  these can be implemented by red-black-trees (theory @{theory RBT}).
    6.20 +  these can be implemented by red-black-trees (theory @{theory "HOL-Library.RBT"}).
    6.21  \<close>
    6.22  
    6.23  end
     7.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Jun 22 18:31:50 2018 +0200
     7.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jun 22 20:31:49 2018 +0200
     7.3 @@ -183,7 +183,7 @@
     7.4  @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
     7.5  
     7.6  Polymorphic types are possible, such as the following option type, modeled after
     7.7 -its homologue from the @{theory Option} theory:
     7.8 +its homologue from the @{theory HOL.Option} theory:
     7.9  \<close>
    7.10  
    7.11  (*<*)
     8.1 --- a/src/Doc/Eisbach/Manual.thy	Fri Jun 22 18:31:50 2018 +0200
     8.2 +++ b/src/Doc/Eisbach/Manual.thy	Fri Jun 22 20:31:49 2018 +0200
     8.3 @@ -896,9 +896,9 @@
     8.4  
     8.5  text \<open>
     8.6    Method tracing is supported by auxiliary print methods provided by @{theory
     8.7 -  Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and
     8.8 -  @{method print_type}. Whenever a print method is evaluated it leaves the
     8.9 -  goal unchanged and writes its argument as tracing output.
    8.10 +  "HOL-Eisbach.Eisbach_Tools"}. These include @{method print_fact}, @{method
    8.11 +  print_term} and @{method print_type}. Whenever a print method is evaluated
    8.12 +  it leaves the goal unchanged and writes its argument as tracing output.
    8.13  
    8.14    Print methods can be combined with the @{method fail} method to investigate
    8.15    the backtracking behaviour of a method.
     9.1 --- a/src/Doc/Eisbach/Preface.thy	Fri Jun 22 18:31:50 2018 +0200
     9.2 +++ b/src/Doc/Eisbach/Preface.thy	Fri Jun 22 20:31:49 2018 +0200
     9.3 @@ -32,10 +32,10 @@
     9.4    well as the @{method match} method, as well as discussing their integration
     9.5    with existing Isar concepts such as @{command named_theorems}.
     9.6  
     9.7 -  These commands are provided by theory @{theory "Eisbach"} (see
     9.8 -  \<^file>\<open>~~/src/HOL/Eisbach/Eisbach.thy\<close>): it needs to be imported by all Eisbach
     9.9 -  applications. Theory theory @{theory "Eisbach_Tools"} provides additional
    9.10 -  proof methods and attributes that are occasionally useful.
    9.11 +  These commands are provided by theory @{theory "HOL-Eisbach.Eisbach"}: it
    9.12 +  needs to be imported by all Eisbach applications. Theory theory @{theory
    9.13 +  "HOL-Eisbach.Eisbach_Tools"} provides additional proof methods and
    9.14 +  attributes that are occasionally useful.
    9.15  \<close>
    9.16  
    9.17  end
    10.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Jun 22 18:31:50 2018 +0200
    10.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Jun 22 20:31:49 2018 +0200
    10.3 @@ -221,8 +221,8 @@
    10.4    \<^descr> \<open>@{theory_text s}\<close> prints uninterpreted theory source text \<open>s\<close>, i.e.\
    10.5    outer syntax with command keywords and other tokens.
    10.6  
    10.7 -  \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is guaranteed to refer to a valid
    10.8 -  ancestor theory in the current context.
    10.9 +  \<^descr> \<open>@{theory A}\<close> prints the session-qualified theory name \<open>A\<close>, which is
   10.10 +  guaranteed to refer to a valid ancestor theory in the current context.
   10.11  
   10.12    \<^descr> \<open>@{thm a\<^sub>1 \<dots> a\<^sub>n}\<close> prints theorems \<open>a\<^sub>1 \<dots> a\<^sub>n\<close>. Full fact expressions are
   10.13    allowed here, including attributes (\secref{sec:syn-att}).
    11.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jun 22 18:31:50 2018 +0200
    11.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jun 22 20:31:49 2018 +0200
    11.3 @@ -1875,7 +1875,7 @@
    11.4      class @{class random} generates a pseudo-random value of the given size
    11.5      and a lazy term reconstruction of the value in the type @{typ
    11.6      Code_Evaluation.term}. A pseudo-randomness generator is defined in theory
    11.7 -    @{theory Random}.
    11.8 +    @{theory HOL.Random}.
    11.9  
   11.10      \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
   11.11      "runciman-naylor-lindblad"} using the type classes @{class narrowing} and
   11.12 @@ -1997,7 +1997,7 @@
   11.13    the definition of syntatic constructs (usually extralogical, i.e., processed
   11.14    and stripped during type inference), that should not be destroyed by the
   11.15    insertion of coercions (see, for example, the setup for the case syntax in
   11.16 -  @{theory Ctr_Sugar}).
   11.17 +  @{theory HOL.Ctr_Sugar}).
   11.18  
   11.19    \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference
   11.20    algorithm.
    12.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jun 22 18:31:50 2018 +0200
    12.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jun 22 20:31:49 2018 +0200
    12.3 @@ -1215,12 +1215,12 @@
    12.4  
    12.5    \<^item> Iterated replacement via recursive @{command translations}. For example,
    12.6    consider list enumeration @{term "[a, b, c, d]"} as defined in theory
    12.7 -  @{theory List} in Isabelle/HOL.
    12.8 +  @{theory HOL.List}.
    12.9  
   12.10    \<^item> Change of binding status of variables: anything beyond the built-in
   12.11    @{keyword "binder"} mixfix annotation requires explicit syntax translations.
   12.12    For example, consider the set comprehension syntax @{term "{x. P}"} as
   12.13 -  defined in theory @{theory Set} in Isabelle/HOL.
   12.14 +  defined in theory @{theory HOL.Set}.
   12.15  \<close>
   12.16  
   12.17  
    13.1 --- a/src/Doc/Main/Main_Doc.thy	Fri Jun 22 18:31:50 2018 +0200
    13.2 +++ b/src/Doc/Main/Main_Doc.thy	Fri Jun 22 20:31:49 2018 +0200
    13.3 @@ -78,7 +78,7 @@
    13.4  \section*{Lattices}
    13.5  
    13.6  Classes semilattice, lattice, distributive lattice and complete lattice (the
    13.7 -latter in theory @{theory Set}).
    13.8 +latter in theory @{theory HOL.Set}).
    13.9  
   13.10  \begin{tabular}{@ {} l @ {~::~} l @ {}}
   13.11  @{const Lattices.inf} & @{typeof Lattices.inf}\\
   13.12 @@ -182,7 +182,7 @@
   13.13  
   13.14  \section*{Fixed Points}
   13.15  
   13.16 -Theory: @{theory Inductive}.
   13.17 +Theory: @{theory HOL.Inductive}.
   13.18  
   13.19  Least and greatest fixed points in a complete lattice @{typ 'a}:
   13.20  
   13.21 @@ -303,8 +303,8 @@
   13.22  
   13.23  \section*{Algebra}
   13.24  
   13.25 -Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory
   13.26 -Divides} define a large collection of classes describing common algebraic
   13.27 +Theories @{theory HOL.Groups}, @{theory HOL.Rings}, @{theory HOL.Fields} and @{theory
   13.28 +HOL.Divides} define a large collection of classes describing common algebraic
   13.29  structures from semigroups up to fields. Everything is done in terms of
   13.30  overloaded operators:
   13.31  
   13.32 @@ -454,7 +454,7 @@
   13.33  \end{supertabular}
   13.34  
   13.35  
   13.36 -\section*{Set\_Interval} % @{theory Set_Interval}
   13.37 +\section*{Set\_Interval} % @{theory HOL.Set_Interval}
   13.38  
   13.39  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
   13.40  @{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
    14.1 --- a/src/Doc/Tutorial/Types/Axioms.thy	Fri Jun 22 18:31:50 2018 +0200
    14.2 +++ b/src/Doc/Tutorial/Types/Axioms.thy	Fri Jun 22 20:31:49 2018 +0200
    14.3 @@ -254,7 +254,7 @@
    14.4  \emph{with} axioms.
    14.5  
    14.6  Further note that classes may contain axioms but \emph{no} operations.
    14.7 -An example is class @{class finite} from theory @{theory Finite_Set}
    14.8 +An example is class @{class finite} from theory @{theory "HOL.Finite_Set"}
    14.9  which specifies a type to be finite: @{lemma [source] "finite (UNIV :: 'a::finite
   14.10  set)" by (fact finite_UNIV)}.\<close>
   14.11  
    15.1 --- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Jun 22 18:31:50 2018 +0200
    15.2 +++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Jun 22 20:31:49 2018 +0200
    15.3 @@ -328,9 +328,9 @@
    15.4  
    15.5      \<^item> The concrete additive inverse operation emerges through
    15.6  
    15.7 -      \<^item> @{command class} @{class group_add} = @{class minus} + @{class uminus} + @{class monoid_add} (in @{theory Groups}) \\
    15.8 +      \<^item> @{command class} @{class group_add} = @{class minus} + @{class uminus} + @{class monoid_add} (in @{theory HOL.Groups}) \\
    15.9  
   15.10 -      \<^item> @{command class} @{class ab_group_add} = @{class minus} + @{class uminus} + @{class comm_monoid_add} (in @{theory Groups})
   15.11 +      \<^item> @{command class} @{class ab_group_add} = @{class minus} + @{class uminus} + @{class comm_monoid_add} (in @{theory HOL.Groups})
   15.12  
   15.13        and corresponding interpretation of locale @{locale group}, yielding e.g.
   15.14  
    16.1 --- a/src/HOL/Algebra/AbelCoset.thy	Fri Jun 22 18:31:50 2018 +0200
    16.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Fri Jun 22 20:31:49 2018 +0200
    16.3 @@ -10,7 +10,7 @@
    16.4  
    16.5  subsubsection \<open>Definitions\<close>
    16.6  
    16.7 -text \<open>Hiding \<open><+>\<close> from @{theory Sum_Type} until I come
    16.8 +text \<open>Hiding \<open><+>\<close> from @{theory HOL.Sum_Type} until I come
    16.9    up with better syntax here\<close>
   16.10  
   16.11  no_notation Sum_Type.Plus (infixr "<+>" 65)
    17.1 --- a/src/HOL/Algebra/Sylow.thy	Fri Jun 22 18:31:50 2018 +0200
    17.2 +++ b/src/HOL/Algebra/Sylow.thy	Fri Jun 22 20:31:49 2018 +0200
    17.3 @@ -8,7 +8,7 @@
    17.4  
    17.5  text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
    17.6  
    17.7 -text \<open>The combinatorial argument is in theory @{theory Exponent}.\<close>
    17.8 +text \<open>The combinatorial argument is in theory @{theory "HOL-Algebra.Exponent"}.\<close>
    17.9  
   17.10  lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
   17.11    for c :: nat
    18.1 --- a/src/HOL/Analysis/Measure_Space.thy	Fri Jun 22 18:31:50 2018 +0200
    18.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Jun 22 20:31:49 2018 +0200
    18.3 @@ -55,8 +55,8 @@
    18.4  qed
    18.5  
    18.6  text \<open>
    18.7 -  The type for emeasure spaces is already defined in @{theory Sigma_Algebra}, as it is also used to
    18.8 -  represent sigma algebras (with an arbitrary emeasure).
    18.9 +  The type for emeasure spaces is already defined in @{theory "HOL-Analysis.Sigma_Algebra"}, as it
   18.10 +  is also used to represent sigma algebras (with an arbitrary emeasure).
   18.11  \<close>
   18.12  
   18.13  subsection%unimportant "Extend binary sets"
   18.14 @@ -95,7 +95,7 @@
   18.15  
   18.16  text \<open>
   18.17    The definitions for @{const positive} and @{const countably_additive} should be here, by they are
   18.18 -  necessary to define @{typ "'a measure"} in @{theory Sigma_Algebra}.
   18.19 +  necessary to define @{typ "'a measure"} in @{theory "HOL-Analysis.Sigma_Algebra"}.
   18.20  \<close>
   18.21  
   18.22  definition subadditive where
    19.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Jun 22 18:31:50 2018 +0200
    19.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Jun 22 20:31:49 2018 +0200
    19.3 @@ -17,7 +17,7 @@
    19.4    "HOL-ex.Records"
    19.5  begin
    19.6  
    19.7 -text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    19.8 +text \<open>Drop technical stuff from @{theory HOL.Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    19.9  
   19.10  setup \<open>
   19.11  fn thy =>
    20.1 --- a/src/HOL/Data_Structures/Set2_Join.thy	Fri Jun 22 18:31:50 2018 +0200
    20.2 +++ b/src/HOL/Data_Structures/Set2_Join.thy	Fri Jun 22 20:31:49 2018 +0200
    20.3 @@ -12,7 +12,7 @@
    20.4  All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close>
    20.5  and an element \<open>x\<close> such that \<open>l < x < r\<close>.
    20.6  
    20.7 -The theory is based on theory @{theory Tree2} where nodes have an additional field.
    20.8 +The theory is based on theory @{theory "HOL-Data_Structures.Tree2"} where nodes have an additional field.
    20.9  This field is ignored here but it means that this theory can be instantiated
   20.10  with red-black trees (see theory @{file "Set2_Join_RBT.thy"}) and other balanced trees.
   20.11  This approach is very concrete and fixes the type of trees.
    21.1 --- a/src/HOL/Groebner_Basis.thy	Fri Jun 22 18:31:50 2018 +0200
    21.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Jun 22 20:31:49 2018 +0200
    21.3 @@ -10,9 +10,9 @@
    21.4  
    21.5  subsection \<open>Groebner Bases\<close>
    21.6  
    21.7 -lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL}\<close>
    21.8 +lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL.HOL}\<close>
    21.9  
   21.10 -lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL}\<close>
   21.11 +lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL.HOL}\<close>
   21.12    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
   21.13    "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   21.14    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
    22.1 --- a/src/HOL/IMP/Abs_Int0.thy	Fri Jun 22 18:31:50 2018 +0200
    22.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Fri Jun 22 20:31:49 2018 +0200
    22.3 @@ -7,7 +7,7 @@
    22.4  subsection "Orderings"
    22.5  
    22.6  text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
    22.7 -defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
    22.8 +defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}.
    22.9  If you view this theory with jedit, just click on the names to get there.\<close>
   22.10  
   22.11  class semilattice_sup_top = semilattice_sup + order_top
    23.1 --- a/src/HOL/IMP/Compiler2.thy	Fri Jun 22 18:31:50 2018 +0200
    23.2 +++ b/src/HOL/IMP/Compiler2.thy	Fri Jun 22 20:31:49 2018 +0200
    23.3 @@ -6,7 +6,7 @@
    23.4  
    23.5  text \<open>
    23.6  The preservation of the source code semantics is already shown in the 
    23.7 -parent theory @{theory Compiler}. This here shows the second direction.
    23.8 +parent theory @{theory "HOL-IMP.Compiler"}. This here shows the second direction.
    23.9  \<close>
   23.10  
   23.11  section \<open>Compiler Correctness, Reverse Direction\<close>
    24.1 --- a/src/HOL/IMP/Live_True.thy	Fri Jun 22 18:31:50 2018 +0200
    24.2 +++ b/src/HOL/IMP/Live_True.thy	Fri Jun 22 20:31:49 2018 +0200
    24.3 @@ -115,7 +115,7 @@
    24.4  qed auto
    24.5  
    24.6  text\<open>Make @{const L} executable by replacing @{const lfp} with the @{const
    24.7 -while} combinator from theory @{theory While_Combinator}. The @{const while}
    24.8 +while} combinator from theory @{theory "HOL-Library.While_Combinator"}. The @{const while}
    24.9  combinator obeys the recursion equation
   24.10  @{thm[display] While_Combinator.while_unfold[no_vars]}
   24.11  and is thus executable.\<close>
    25.1 --- a/src/HOL/Library/Code_Test.thy	Fri Jun 22 18:31:50 2018 +0200
    25.2 +++ b/src/HOL/Library/Code_Test.thy	Fri Jun 22 20:31:49 2018 +0200
    25.3 @@ -132,7 +132,7 @@
    25.4    "xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
    25.5    "xml_of_term (Code_Evaluation.App t1 t2)  = [xml.tagged (STR ''5'') None [xml.node (xml_of_term t1), xml.node (xml_of_term t2)]]"
    25.6    "xml_of_term (Code_Evaluation.Abs x ty t) = [xml.tagged (STR ''4'') (Some x) [xml.node (xml_of_typ ty), xml.node (xml_of_term t)]]"
    25.7 -  \<comment> \<open>FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
    25.8 +  \<comment> \<open>FIXME: @{const Code_Evaluation.Free} is used only in @{theory "HOL.Quickcheck_Narrowing"} to represent
    25.9      uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.\<close>
   25.10    "xml_of_term (Code_Evaluation.Free x ty)  = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
   25.11  by(simp_all add: xml_of_term_def xml_tree_anything)
    26.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Jun 22 18:31:50 2018 +0200
    26.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Jun 22 20:31:49 2018 +0200
    26.3 @@ -12,8 +12,11 @@
    26.4  imports Complex_Main Extended_Nat Liminf_Limsup
    26.5  begin
    26.6  
    26.7 -text \<open>This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
    26.8 -AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.\<close>
    26.9 +text \<open>
   26.10 +  This should be part of @{theory "HOL-Library.Extended_Nat"} or @{theory
   26.11 +  "HOL-Library.Order_Continuity"}, but then the AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload
   26.12 +  certain named from @{theory Complex_Main}.
   26.13 +\<close>
   26.14  
   26.15  lemma incseq_sumI2:
   26.16    fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"
    27.1 --- a/src/HOL/Library/RBT_Mapping.thy	Fri Jun 22 18:31:50 2018 +0200
    27.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Fri Jun 22 20:31:49 2018 +0200
    27.3 @@ -113,7 +113,7 @@
    27.4  text \<open>
    27.5    This theory defines abstract red-black trees as an efficient
    27.6    representation of finite maps, backed by the implementation
    27.7 -  in @{theory RBT_Impl}.
    27.8 +  in @{theory "HOL-Library.RBT_Impl"}.
    27.9  \<close>
   27.10  
   27.11  subsection \<open>Data type and invariant\<close>
    28.1 --- a/src/HOL/Library/Tree_Multiset.thy	Fri Jun 22 18:31:50 2018 +0200
    28.2 +++ b/src/HOL/Library/Tree_Multiset.thy	Fri Jun 22 20:31:49 2018 +0200
    28.3 @@ -6,9 +6,11 @@
    28.4  imports Multiset Tree
    28.5  begin
    28.6  
    28.7 -text\<open>Kept separate from theory @{theory Tree} to avoid importing all of
    28.8 -theory @{theory Multiset} into @{theory Tree}. Should be merged if
    28.9 -@{theory Multiset} ever becomes part of @{theory Main}.\<close>
   28.10 +text \<open>
   28.11 +  Kept separate from theory @{theory "HOL-Library.Tree"} to avoid importing all of theory @{theory
   28.12 +  "HOL-Library.Multiset"} into @{theory "HOL-Library.Tree"}. Should be merged if @{theory
   28.13 +  "HOL-Library.Multiset"} ever becomes part of @{theory Main}.
   28.14 +\<close>
   28.15  
   28.16  fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
   28.17  "mset_tree Leaf = {#}" |
    29.1 --- a/src/HOL/Library/Tree_Real.thy	Fri Jun 22 18:31:50 2018 +0200
    29.2 +++ b/src/HOL/Library/Tree_Real.thy	Fri Jun 22 20:31:49 2018 +0200
    29.3 @@ -6,8 +6,10 @@
    29.4    Tree
    29.5  begin
    29.6  
    29.7 -text \<open>This theory is separate from @{theory Tree} because the former is discrete and builds on
    29.8 -@{theory Main} whereas this theory builds on @{theory Complex_Main}.\<close>
    29.9 +text \<open>
   29.10 +  This theory is separate from @{theory "HOL-Library.Tree"} because the former is discrete and
   29.11 +  builds on @{theory Main} whereas this theory builds on @{theory Complex_Main}.
   29.12 +\<close>
   29.13  
   29.14  
   29.15  lemma size1_height_log: "log 2 (size1 t) \<le> height t"
    30.1 --- a/src/HOL/Order_Relation.thy	Fri Jun 22 18:31:50 2018 +0200
    30.2 +++ b/src/HOL/Order_Relation.thy	Fri Jun 22 20:31:49 2018 +0200
    30.3 @@ -351,7 +351,7 @@
    30.4  subsection \<open>Variations on Well-Founded Relations\<close>
    30.5  
    30.6  text \<open>
    30.7 -  This subsection contains some variations of the results from @{theory Wellfounded}:
    30.8 +  This subsection contains some variations of the results from \<^theory>\<open>HOL.Wellfounded\<close>:
    30.9      \<^item> means for slightly more direct definitions by well-founded recursion;
   30.10      \<^item> variations of well-founded induction;
   30.11      \<^item> means for proving a linear order to be a well-order.
    31.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jun 22 18:31:50 2018 +0200
    31.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jun 22 20:31:49 2018 +0200
    31.3 @@ -54,7 +54,7 @@
    31.4  where
    31.5    "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f \<circ> c) cs)"
    31.6  
    31.7 -subsubsection \<open>From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms\<close>
    31.8 +subsubsection \<open>From narrowing's deep representation of terms to @{theory HOL.Code_Evaluation}'s terms\<close>
    31.9  
   31.10  class partial_term_of = typerep +
   31.11    fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
    32.1 --- a/src/HOL/Real.thy	Fri Jun 22 18:31:50 2018 +0200
    32.2 +++ b/src/HOL/Real.thy	Fri Jun 22 20:31:49 2018 +0200
    32.3 @@ -1387,7 +1387,7 @@
    32.4    for d1 d2 :: real
    32.5    by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
    32.6  
    32.7 -text \<open>Similar results are proved in @{theory Fields}\<close>
    32.8 +text \<open>Similar results are proved in @{theory HOL.Fields}\<close>
    32.9  lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
   32.10    for x y :: real
   32.11    by auto
    33.1 --- a/src/HOL/ex/Erdoes_Szekeres.thy	Fri Jun 22 18:31:50 2018 +0200
    33.2 +++ b/src/HOL/ex/Erdoes_Szekeres.thy	Fri Jun 22 20:31:49 2018 +0200
    33.3 @@ -8,7 +8,7 @@
    33.4  imports Main
    33.5  begin
    33.6  
    33.7 -subsection \<open>Addition to @{theory Lattices_Big} Theory\<close>
    33.8 +subsection \<open>Addition to @{theory HOL.Lattices_Big} Theory\<close>
    33.9  
   33.10  lemma Max_gr:
   33.11    assumes "finite A"
   33.12 @@ -16,7 +16,7 @@
   33.13    shows "x < Max A"
   33.14  using assms Max_ge less_le_trans by blast
   33.15  
   33.16 -subsection \<open>Additions to @{theory Finite_Set} Theory\<close>
   33.17 +subsection \<open>Additions to @{theory HOL.Finite_Set} Theory\<close>
   33.18  
   33.19  lemma obtain_subset_with_card_n:
   33.20    assumes "n \<le> card S"
    34.1 --- a/src/HOL/ex/Sum_of_Powers.thy	Fri Jun 22 18:31:50 2018 +0200
    34.2 +++ b/src/HOL/ex/Sum_of_Powers.thy	Fri Jun 22 20:31:49 2018 +0200
    34.3 @@ -5,7 +5,7 @@
    34.4  imports Complex_Main
    34.5  begin
    34.6  
    34.7 -subsection \<open>Additions to @{theory Binomial} Theory\<close>
    34.8 +subsection \<open>Additions to @{theory HOL.Binomial} Theory\<close>
    34.9  
   34.10  lemma (in field_char_0) one_plus_of_nat_neq_zero [simp]:
   34.11    "1 + of_nat n \<noteq> 0"
    35.1 --- a/src/Pure/Thy/document_antiquotations.ML	Fri Jun 22 18:31:50 2018 +0200
    35.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jun 22 20:31:49 2018 +0200
    35.3 @@ -61,7 +61,7 @@
    35.4  fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
    35.5  
    35.6  fun pretty_theory ctxt (name, pos) =
    35.7 -  (Theory.check {long = false} ctxt (name, pos); Pretty.str name);
    35.8 +  (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
    35.9  
   35.10  val basic_entity = Thy_Output.antiquotation_pretty_source;
   35.11  
    36.1 --- a/src/Pure/theory.ML	Fri Jun 22 18:31:50 2018 +0200
    36.2 +++ b/src/Pure/theory.ML	Fri Jun 22 20:31:49 2018 +0200
    36.3 @@ -143,7 +143,7 @@
    36.4                Completion.make (name, pos)
    36.5                  (fn completed =>
    36.6                    map (Context.theory_name' long) (ancestors_of thy)
    36.7 -                  |> filter completed
    36.8 +                  |> filter (completed o Long_Name.base_name)
    36.9                    |> sort_strings
   36.10                    |> map (fn a => (a, (Markup.theoryN, a))));
   36.11              val report = Markup.markup_report (Completion.reported_text completion);