--- a/NEWS Fri Jun 22 18:31:50 2018 +0200
+++ b/NEWS Fri Jun 22 20:31:49 2018 +0200
@@ -167,6 +167,10 @@
* Document preparation with skip_proofs option now preserves the content
more accurately: only terminal proof steps ('by' etc.) are skipped.
+* Document antiquotation @{theory name} requires the long
+session-qualified theory name: this is what users reading the text
+normally need to import.
+
* Document antiquotation @{session name} checks and prints the given
session name verbatim.
--- a/src/Doc/Codegen/Adaptation.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Fri Jun 22 20:31:49 2018 +0200
@@ -151,7 +151,7 @@
subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close>
text \<open>
- The @{theory HOL} @{theory Main} theory already provides a code
+ The @{theory Main} theory of Isabelle/HOL already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
@@ -160,7 +160,7 @@
\begin{description}
- \item[@{theory "Code_Numeral"}] provides additional numeric
+ \item[@{theory "HOL.Code_Numeral"}] provides additional numeric
types @{typ integer} and @{typ natural} isomorphic to types
@{typ int} and @{typ nat} respectively. Type @{typ integer}
is mapped to target-language built-in integers; @{typ natural}
@@ -168,7 +168,7 @@
Useful for code setups which involve e.g.~indexing
of target-language arrays. Part of @{text "HOL-Main"}.
- \item[@{theory "String"}] provides an additional datatype @{typ
+ \item[@{theory "HOL.String"}] provides an additional datatype @{typ
String.literal} which is isomorphic to lists of 7-bit (ASCII) characters;
@{typ String.literal}s are mapped to target-language strings.
@@ -215,7 +215,7 @@
containing both @{text "Code_Target_Nat"} and
@{text "Code_Target_Int"}.
- \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
+ \item[@{theory "HOL-Library.IArray"}] provides a type @{typ "'a iarray"}
isomorphic to lists but implemented by (effectively immutable)
arrays \emph{in SML only}.
--- a/src/Doc/Codegen/Foundations.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Codegen/Foundations.thy Fri Jun 22 20:31:49 2018 +0200
@@ -11,9 +11,9 @@
components which can be customised individually.
Conceptually all components operate on Isabelle's logic framework
- @{theory Pure}. Practically, the object logic @{theory HOL}
+ Pure. Practically, the object logic HOL
provides the necessary facilities to make use of the code generator,
- mainly since it is an extension of @{theory Pure}.
+ mainly since it is an extension of Isabelle/Pure.
The constellation of the different components is visualized in the
following picture.
--- a/src/Doc/Codegen/Further.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Codegen/Further.thy Fri Jun 22 20:31:49 2018 +0200
@@ -30,7 +30,7 @@
arbitrary ML code as well.
A typical example for @{command code_reflect} can be found in the
- @{theory Predicate} theory.
+ @{theory HOL.Predicate} theory.
\<close>
--- a/src/Doc/Codegen/Introduction.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Codegen/Introduction.thy Fri Jun 22 20:31:49 2018 +0200
@@ -17,7 +17,7 @@
@{cite "scala-overview-tech-report"}.
To profit from this tutorial, some familiarity and experience with
- @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
+ Isabelle/HOL @{cite "isa-tutorial"} and its basic theories is assumed.
\<close>
--- a/src/Doc/Codegen/Refinement.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Codegen/Refinement.thy Fri Jun 22 20:31:49 2018 +0200
@@ -188,7 +188,7 @@
of distinct elements.
The specification of @{typ "'a dlist"} itself can be found in theory
- @{theory Dlist}.
+ @{theory "HOL-Library.Dlist"}.
The first step is to decide on which representation the abstract
type (in our example @{typ "'a dlist"}) should be implemented.
@@ -271,9 +271,9 @@
for the meta theory of datatype refinement involving invariants.
Typical data structures implemented by representations involving
- invariants are available in the library, theory @{theory Mapping}
+ invariants are available in the library, theory @{theory "HOL-Library.Mapping"}
specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
- these can be implemented by red-black-trees (theory @{theory RBT}).
+ these can be implemented by red-black-trees (theory @{theory "HOL-Library.RBT"}).
\<close>
end
--- a/src/Doc/Datatypes/Datatypes.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Jun 22 20:31:49 2018 +0200
@@ -183,7 +183,7 @@
@{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
Polymorphic types are possible, such as the following option type, modeled after
-its homologue from the @{theory Option} theory:
+its homologue from the @{theory HOL.Option} theory:
\<close>
(*<*)
--- a/src/Doc/Eisbach/Manual.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Eisbach/Manual.thy Fri Jun 22 20:31:49 2018 +0200
@@ -896,9 +896,9 @@
text \<open>
Method tracing is supported by auxiliary print methods provided by @{theory
- Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and
- @{method print_type}. Whenever a print method is evaluated it leaves the
- goal unchanged and writes its argument as tracing output.
+ "HOL-Eisbach.Eisbach_Tools"}. These include @{method print_fact}, @{method
+ print_term} and @{method print_type}. Whenever a print method is evaluated
+ it leaves the goal unchanged and writes its argument as tracing output.
Print methods can be combined with the @{method fail} method to investigate
the backtracking behaviour of a method.
--- a/src/Doc/Eisbach/Preface.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Eisbach/Preface.thy Fri Jun 22 20:31:49 2018 +0200
@@ -32,10 +32,10 @@
well as the @{method match} method, as well as discussing their integration
with existing Isar concepts such as @{command named_theorems}.
- These commands are provided by theory @{theory "Eisbach"} (see
- \<^file>\<open>~~/src/HOL/Eisbach/Eisbach.thy\<close>): it needs to be imported by all Eisbach
- applications. Theory theory @{theory "Eisbach_Tools"} provides additional
- proof methods and attributes that are occasionally useful.
+ These commands are provided by theory @{theory "HOL-Eisbach.Eisbach"}: it
+ needs to be imported by all Eisbach applications. Theory theory @{theory
+ "HOL-Eisbach.Eisbach_Tools"} provides additional proof methods and
+ attributes that are occasionally useful.
\<close>
end
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Jun 22 20:31:49 2018 +0200
@@ -221,8 +221,8 @@
\<^descr> \<open>@{theory_text s}\<close> prints uninterpreted theory source text \<open>s\<close>, i.e.\
outer syntax with command keywords and other tokens.
- \<^descr> \<open>@{theory A}\<close> prints the name \<open>A\<close>, which is guaranteed to refer to a valid
- ancestor theory in the current context.
+ \<^descr> \<open>@{theory A}\<close> prints the session-qualified theory name \<open>A\<close>, which is
+ guaranteed to refer to a valid ancestor theory in the current context.
\<^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
allowed here, including attributes (\secref{sec:syn-att}).
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Jun 22 20:31:49 2018 +0200
@@ -1875,7 +1875,7 @@
class @{class random} generates a pseudo-random value of the given size
and a lazy term reconstruction of the value in the type @{typ
Code_Evaluation.term}. A pseudo-randomness generator is defined in theory
- @{theory Random}.
+ @{theory HOL.Random}.
\<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
"runciman-naylor-lindblad"} using the type classes @{class narrowing} and
@@ -1997,7 +1997,7 @@
the definition of syntatic constructs (usually extralogical, i.e., processed
and stripped during type inference), that should not be destroyed by the
insertion of coercions (see, for example, the setup for the case syntax in
- @{theory Ctr_Sugar}).
+ @{theory HOL.Ctr_Sugar}).
\<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference
algorithm.
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Jun 22 20:31:49 2018 +0200
@@ -1215,12 +1215,12 @@
\<^item> Iterated replacement via recursive @{command translations}. For example,
consider list enumeration @{term "[a, b, c, d]"} as defined in theory
- @{theory List} in Isabelle/HOL.
+ @{theory HOL.List}.
\<^item> Change of binding status of variables: anything beyond the built-in
@{keyword "binder"} mixfix annotation requires explicit syntax translations.
For example, consider the set comprehension syntax @{term "{x. P}"} as
- defined in theory @{theory Set} in Isabelle/HOL.
+ defined in theory @{theory HOL.Set}.
\<close>
--- a/src/Doc/Main/Main_Doc.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy Fri Jun 22 20:31:49 2018 +0200
@@ -78,7 +78,7 @@
\section*{Lattices}
Classes semilattice, lattice, distributive lattice and complete lattice (the
-latter in theory @{theory Set}).
+latter in theory @{theory HOL.Set}).
\begin{tabular}{@ {} l @ {~::~} l @ {}}
@{const Lattices.inf} & @{typeof Lattices.inf}\\
@@ -182,7 +182,7 @@
\section*{Fixed Points}
-Theory: @{theory Inductive}.
+Theory: @{theory HOL.Inductive}.
Least and greatest fixed points in a complete lattice @{typ 'a}:
@@ -303,8 +303,8 @@
\section*{Algebra}
-Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory
-Divides} define a large collection of classes describing common algebraic
+Theories @{theory HOL.Groups}, @{theory HOL.Rings}, @{theory HOL.Fields} and @{theory
+HOL.Divides} define a large collection of classes describing common algebraic
structures from semigroups up to fields. Everything is done in terms of
overloaded operators:
@@ -454,7 +454,7 @@
\end{supertabular}
-\section*{Set\_Interval} % @{theory Set_Interval}
+\section*{Set\_Interval} % @{theory HOL.Set_Interval}
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
--- a/src/Doc/Tutorial/Types/Axioms.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Tutorial/Types/Axioms.thy Fri Jun 22 20:31:49 2018 +0200
@@ -254,7 +254,7 @@
\emph{with} axioms.
Further note that classes may contain axioms but \emph{no} operations.
-An example is class @{class finite} from theory @{theory Finite_Set}
+An example is class @{class finite} from theory @{theory "HOL.Finite_Set"}
which specifies a type to be finite: @{lemma [source] "finite (UNIV :: 'a::finite
set)" by (fact finite_UNIV)}.\<close>
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Jun 22 20:31:49 2018 +0200
@@ -328,9 +328,9 @@
\<^item> The concrete additive inverse operation emerges through
- \<^item> @{command class} @{class group_add} = @{class minus} + @{class uminus} + @{class monoid_add} (in @{theory Groups}) \\
+ \<^item> @{command class} @{class group_add} = @{class minus} + @{class uminus} + @{class monoid_add} (in @{theory HOL.Groups}) \\
- \<^item> @{command class} @{class ab_group_add} = @{class minus} + @{class uminus} + @{class comm_monoid_add} (in @{theory Groups})
+ \<^item> @{command class} @{class ab_group_add} = @{class minus} + @{class uminus} + @{class comm_monoid_add} (in @{theory HOL.Groups})
and corresponding interpretation of locale @{locale group}, yielding e.g.
--- a/src/HOL/Algebra/AbelCoset.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Fri Jun 22 20:31:49 2018 +0200
@@ -10,7 +10,7 @@
subsubsection \<open>Definitions\<close>
-text \<open>Hiding \<open><+>\<close> from @{theory Sum_Type} until I come
+text \<open>Hiding \<open><+>\<close> from @{theory HOL.Sum_Type} until I come
up with better syntax here\<close>
no_notation Sum_Type.Plus (infixr "<+>" 65)
--- a/src/HOL/Algebra/Sylow.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Algebra/Sylow.thy Fri Jun 22 20:31:49 2018 +0200
@@ -8,7 +8,7 @@
text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
-text \<open>The combinatorial argument is in theory @{theory Exponent}.\<close>
+text \<open>The combinatorial argument is in theory @{theory "HOL-Algebra.Exponent"}.\<close>
lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
for c :: nat
--- a/src/HOL/Analysis/Measure_Space.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Jun 22 20:31:49 2018 +0200
@@ -55,8 +55,8 @@
qed
text \<open>
- The type for emeasure spaces is already defined in @{theory Sigma_Algebra}, as it is also used to
- represent sigma algebras (with an arbitrary emeasure).
+ The type for emeasure spaces is already defined in @{theory "HOL-Analysis.Sigma_Algebra"}, as it
+ is also used to represent sigma algebras (with an arbitrary emeasure).
\<close>
subsection%unimportant "Extend binary sets"
@@ -95,7 +95,7 @@
text \<open>
The definitions for @{const positive} and @{const countably_additive} should be here, by they are
- necessary to define @{typ "'a measure"} in @{theory Sigma_Algebra}.
+ necessary to define @{typ "'a measure"} in @{theory "HOL-Analysis.Sigma_Algebra"}.
\<close>
definition subadditive where
--- a/src/HOL/Codegenerator_Test/Candidates.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Fri Jun 22 20:31:49 2018 +0200
@@ -17,7 +17,7 @@
"HOL-ex.Records"
begin
-text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
+text \<open>Drop technical stuff from @{theory HOL.Quickcheck_Narrowing} which is tailored towards Haskell\<close>
setup \<open>
fn thy =>
--- a/src/HOL/Data_Structures/Set2_Join.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Fri Jun 22 20:31:49 2018 +0200
@@ -12,7 +12,7 @@
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>
and an element \<open>x\<close> such that \<open>l < x < r\<close>.
-The theory is based on theory @{theory Tree2} where nodes have an additional field.
+The theory is based on theory @{theory "HOL-Data_Structures.Tree2"} where nodes have an additional field.
This field is ignored here but it means that this theory can be instantiated
with red-black trees (see theory @{file "Set2_Join_RBT.thy"}) and other balanced trees.
This approach is very concrete and fixes the type of trees.
--- a/src/HOL/Groebner_Basis.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Groebner_Basis.thy Fri Jun 22 20:31:49 2018 +0200
@@ -10,9 +10,9 @@
subsection \<open>Groebner Bases\<close>
-lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL}\<close>
+lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL.HOL}\<close>
-lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL}\<close>
+lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL.HOL}\<close>
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
"(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
--- a/src/HOL/IMP/Abs_Int0.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Fri Jun 22 20:31:49 2018 +0200
@@ -7,7 +7,7 @@
subsection "Orderings"
text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
-defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
+defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}.
If you view this theory with jedit, just click on the names to get there.\<close>
class semilattice_sup_top = semilattice_sup + order_top
--- a/src/HOL/IMP/Compiler2.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/IMP/Compiler2.thy Fri Jun 22 20:31:49 2018 +0200
@@ -6,7 +6,7 @@
text \<open>
The preservation of the source code semantics is already shown in the
-parent theory @{theory Compiler}. This here shows the second direction.
+parent theory @{theory "HOL-IMP.Compiler"}. This here shows the second direction.
\<close>
section \<open>Compiler Correctness, Reverse Direction\<close>
--- a/src/HOL/IMP/Live_True.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/IMP/Live_True.thy Fri Jun 22 20:31:49 2018 +0200
@@ -115,7 +115,7 @@
qed auto
text\<open>Make @{const L} executable by replacing @{const lfp} with the @{const
-while} combinator from theory @{theory While_Combinator}. The @{const while}
+while} combinator from theory @{theory "HOL-Library.While_Combinator"}. The @{const while}
combinator obeys the recursion equation
@{thm[display] While_Combinator.while_unfold[no_vars]}
and is thus executable.\<close>
--- a/src/HOL/Library/Code_Test.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Library/Code_Test.thy Fri Jun 22 20:31:49 2018 +0200
@@ -132,7 +132,7 @@
"xml_of_term (Code_Evaluation.Const x ty) = [xml.tagged (STR ''0'') (Some x) (xml_of_typ ty)]"
"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)]]"
"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)]]"
- \<comment> \<open>FIXME: @{const Code_Evaluation.Free} is used only in @{theory Quickcheck_Narrowing} to represent
+ \<comment> \<open>FIXME: @{const Code_Evaluation.Free} is used only in @{theory "HOL.Quickcheck_Narrowing"} to represent
uninstantiated parameters in constructors. Here, we always translate them to @{ML Free} variables.\<close>
"xml_of_term (Code_Evaluation.Free x ty) = [xml.tagged (STR ''1'') (Some x) (xml_of_typ ty)]"
by(simp_all add: xml_of_term_def xml_tree_anything)
--- a/src/HOL/Library/Extended_Real.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Jun 22 20:31:49 2018 +0200
@@ -12,8 +12,11 @@
imports Complex_Main Extended_Nat Liminf_Limsup
begin
-text \<open>This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
-AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.\<close>
+text \<open>
+ This should be part of @{theory "HOL-Library.Extended_Nat"} or @{theory
+ "HOL-Library.Order_Continuity"}, but then the AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload
+ certain named from @{theory Complex_Main}.
+\<close>
lemma incseq_sumI2:
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"
--- a/src/HOL/Library/RBT_Mapping.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy Fri Jun 22 20:31:49 2018 +0200
@@ -113,7 +113,7 @@
text \<open>
This theory defines abstract red-black trees as an efficient
representation of finite maps, backed by the implementation
- in @{theory RBT_Impl}.
+ in @{theory "HOL-Library.RBT_Impl"}.
\<close>
subsection \<open>Data type and invariant\<close>
--- a/src/HOL/Library/Tree_Multiset.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy Fri Jun 22 20:31:49 2018 +0200
@@ -6,9 +6,11 @@
imports Multiset Tree
begin
-text\<open>Kept separate from theory @{theory Tree} to avoid importing all of
-theory @{theory Multiset} into @{theory Tree}. Should be merged if
-@{theory Multiset} ever becomes part of @{theory Main}.\<close>
+text \<open>
+ Kept separate from theory @{theory "HOL-Library.Tree"} to avoid importing all of theory @{theory
+ "HOL-Library.Multiset"} into @{theory "HOL-Library.Tree"}. Should be merged if @{theory
+ "HOL-Library.Multiset"} ever becomes part of @{theory Main}.
+\<close>
fun mset_tree :: "'a tree \<Rightarrow> 'a multiset" where
"mset_tree Leaf = {#}" |
--- a/src/HOL/Library/Tree_Real.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Library/Tree_Real.thy Fri Jun 22 20:31:49 2018 +0200
@@ -6,8 +6,10 @@
Tree
begin
-text \<open>This theory is separate from @{theory Tree} because the former is discrete and builds on
-@{theory Main} whereas this theory builds on @{theory Complex_Main}.\<close>
+text \<open>
+ This theory is separate from @{theory "HOL-Library.Tree"} because the former is discrete and
+ builds on @{theory Main} whereas this theory builds on @{theory Complex_Main}.
+\<close>
lemma size1_height_log: "log 2 (size1 t) \<le> height t"
--- a/src/HOL/Order_Relation.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Order_Relation.thy Fri Jun 22 20:31:49 2018 +0200
@@ -351,7 +351,7 @@
subsection \<open>Variations on Well-Founded Relations\<close>
text \<open>
- This subsection contains some variations of the results from @{theory Wellfounded}:
+ This subsection contains some variations of the results from \<^theory>\<open>HOL.Wellfounded\<close>:
\<^item> means for slightly more direct definitions by well-founded recursion;
\<^item> variations of well-founded induction;
\<^item> means for proving a linear order to be a well-order.
--- a/src/HOL/Quickcheck_Narrowing.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Fri Jun 22 20:31:49 2018 +0200
@@ -54,7 +54,7 @@
where
"map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f \<circ> c) cs)"
-subsubsection \<open>From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms\<close>
+subsubsection \<open>From narrowing's deep representation of terms to @{theory HOL.Code_Evaluation}'s terms\<close>
class partial_term_of = typerep +
fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
--- a/src/HOL/Real.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/Real.thy Fri Jun 22 20:31:49 2018 +0200
@@ -1387,7 +1387,7 @@
for d1 d2 :: real
by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
-text \<open>Similar results are proved in @{theory Fields}\<close>
+text \<open>Similar results are proved in @{theory HOL.Fields}\<close>
lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
for x y :: real
by auto
--- a/src/HOL/ex/Erdoes_Szekeres.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/ex/Erdoes_Szekeres.thy Fri Jun 22 20:31:49 2018 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-subsection \<open>Addition to @{theory Lattices_Big} Theory\<close>
+subsection \<open>Addition to @{theory HOL.Lattices_Big} Theory\<close>
lemma Max_gr:
assumes "finite A"
@@ -16,7 +16,7 @@
shows "x < Max A"
using assms Max_ge less_le_trans by blast
-subsection \<open>Additions to @{theory Finite_Set} Theory\<close>
+subsection \<open>Additions to @{theory HOL.Finite_Set} Theory\<close>
lemma obtain_subset_with_card_n:
assumes "n \<le> card S"
--- a/src/HOL/ex/Sum_of_Powers.thy Fri Jun 22 18:31:50 2018 +0200
+++ b/src/HOL/ex/Sum_of_Powers.thy Fri Jun 22 20:31:49 2018 +0200
@@ -5,7 +5,7 @@
imports Complex_Main
begin
-subsection \<open>Additions to @{theory Binomial} Theory\<close>
+subsection \<open>Additions to @{theory HOL.Binomial} Theory\<close>
lemma (in field_char_0) one_plus_of_nat_neq_zero [simp]:
"1 + of_nat n \<noteq> 0"
--- a/src/Pure/Thy/document_antiquotations.ML Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Jun 22 20:31:49 2018 +0200
@@ -61,7 +61,7 @@
fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
fun pretty_theory ctxt (name, pos) =
- (Theory.check {long = false} ctxt (name, pos); Pretty.str name);
+ (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
val basic_entity = Thy_Output.antiquotation_pretty_source;
--- a/src/Pure/theory.ML Fri Jun 22 18:31:50 2018 +0200
+++ b/src/Pure/theory.ML Fri Jun 22 20:31:49 2018 +0200
@@ -143,7 +143,7 @@
Completion.make (name, pos)
(fn completed =>
map (Context.theory_name' long) (ancestors_of thy)
- |> filter completed
+ |> filter (completed o Long_Name.base_name)
|> sort_strings
|> map (fn a => (a, (Markup.theoryN, a))));
val report = Markup.markup_report (Completion.reported_text completion);