--- a/NEWS Thu Jun 21 23:06:12 2018 +0100
+++ b/NEWS Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Codegen/Foundations.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Codegen/Further.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Codegen/Introduction.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Codegen/Refinement.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Eisbach/Manual.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Eisbach/Preface.thy Fri Jun 22 21:55:20 2018 +0200
@@ -31,6 +31,11 @@
necessarily Isabelle/ML. It covers the usage of the @{command method} as
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 "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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Jun 22 21:55:20 2018 +0200
@@ -167,7 +167,7 @@
@{syntax_def antiquotation_body}:
(@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
options @{syntax text} |
- @@{antiquotation theory} options @{syntax name} |
+ @@{antiquotation theory} options @{syntax embedded} |
@@{antiquotation thm} options styles @{syntax thms} |
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@ -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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Tutorial/Types/Axioms.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Algebra/Sylow.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Data_Structures/Set2_Join.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/IMP/Compiler2.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/IMP/Live_True.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Library/Code_Test.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Library/Tree_Multiset.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Library/Tree_Real.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Order_Relation.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/Real.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/ex/Erdoes_Szekeres.thy Fri Jun 22 21:55:20 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 Thu Jun 21 23:06:12 2018 +0100
+++ b/src/HOL/ex/Sum_of_Powers.thy Fri Jun 22 21:55:20 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/ML/ml_antiquotations.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Fri Jun 22 21:55:20 2018 +0200
@@ -46,13 +46,14 @@
ML_Antiquotation.value \<^binding>\<open>theory\<close>
(Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
- (Theory.check ctxt (name, pos);
- "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
+ (Theory.check {long = false} ctxt (name, pos);
+ "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
+ ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
(Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
- (Theory.check ctxt (name, pos);
+ (Theory.check {long = false} ctxt (name, pos);
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
--- a/src/Pure/Pure.thy Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/Pure.thy Fri Jun 22 21:55:20 2018 +0200
@@ -1269,7 +1269,7 @@
val thy = Toplevel.theory_of st;
val ctxt = Toplevel.context_of st;
fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
- val check = Theory.check ctxt;
+ val check = Theory.check {long = false} ctxt;
in
Thm_Deps.unused_thms
(case opt_range of
--- a/src/Pure/Thy/document_antiquotations.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Jun 22 21:55:20 2018 +0200
@@ -60,7 +60,8 @@
fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
-fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
+fun pretty_theory ctxt (name, pos) =
+ (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
val basic_entity = Thy_Output.antiquotation_pretty_source;
@@ -82,7 +83,7 @@
basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
- basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory #>
+ basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #>
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)
--- a/src/Pure/Thy/sessions.scala Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jun 22 21:55:20 2018 +0200
@@ -459,7 +459,7 @@
val selected_sessions1 =
{
- val sel_sessions1 = session1 :: include_sessions
+ val sel_sessions1 = session1 :: session :: include_sessions
val select_sessions1 =
if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
full_sessions1.selection(Selection(sessions = select_sessions1))
--- a/src/Pure/Thy/thy_output.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Fri Jun 22 21:55:20 2018 +0200
@@ -246,7 +246,7 @@
let
val ctxt' =
Toplevel.presentation_context state'
- handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN);
+ handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
val present = fold (fn (tok, (flag, 0)) =>
fold cons (present_token ctxt' tok)
#> cons (Latex.string flag)
--- a/src/Pure/Tools/thm_deps.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/Tools/thm_deps.ML Fri Jun 22 21:55:20 2018 +0200
@@ -27,7 +27,7 @@
val session =
(case prefix of
a :: _ =>
- (case try (Context.get_theory thy) a of
+ (case try (Context.get_theory {long = false} thy) a of
SOME thy =>
(case Present.theory_qualifier thy of
"" => []
--- a/src/Pure/Tools/thy_deps.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/Tools/thy_deps.ML Fri Jun 22 21:55:20 2018 +0200
@@ -36,6 +36,6 @@
let val thy0 = Proof_Context.theory_of ctxt
in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
-val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
+val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = false});
end;
--- a/src/Pure/context.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/context.ML Fri Jun 22 21:55:20 2018 +0200
@@ -37,11 +37,11 @@
val theory_id_name: theory_id -> string
val theory_long_name: theory -> string
val theory_name: theory -> string
+ val theory_name': {long: bool} -> theory -> string
val PureN: string
val pretty_thy: theory -> Pretty.T
val pretty_abbrev_thy: theory -> Pretty.T
- val get_theory: theory -> string -> theory
- val this_theory: theory -> string -> theory
+ val get_theory: {long: bool} -> theory -> string -> theory
val eq_thy_id: theory_id * theory_id -> bool
val eq_thy: theory * theory -> bool
val proper_subthy_id: theory_id * theory_id -> bool
@@ -160,6 +160,7 @@
val theory_id_name = Long_Name.base_name o theory_id_long_name;
val theory_long_name = #name o history_of;
val theory_name = Long_Name.base_name o theory_long_name;
+fun theory_name' {long} = if long then theory_long_name else theory_name;
val parents_of = #parents o ancestry_of;
val ancestors_of = #ancestors o ancestry_of;
@@ -191,18 +192,14 @@
val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
in Pretty.str_list "{" "}" abbrev end;
-fun get_theory thy name =
- if theory_name thy <> name then
- (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
+fun get_theory long thy name =
+ if theory_name' long thy <> name then
+ (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
SOME thy' => thy'
| NONE => error ("Unknown ancestor theory " ^ quote name))
else if #stage (history_of thy) = finished then thy
else error ("Unfinished theory " ^ quote name);
-fun this_theory thy name =
- if theory_name thy = name then thy
- else get_theory thy name;
-
(* build ids *)
@@ -472,7 +469,7 @@
struct
fun theory_of (Proof.Context (_, thy)) = thy;
fun init_global thy = Proof.Context (init_data thy, thy);
- fun get_global thy name = init_global (get_theory thy name);
+ fun get_global thy name = init_global (get_theory {long = false} thy name);
end;
structure Proof_Data =
--- a/src/Pure/theory.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Pure/theory.ML Fri Jun 22 21:55:20 2018 +0200
@@ -14,7 +14,7 @@
val install_pure: theory -> unit
val get_pure: unit -> theory
val get_markup: theory -> Markup.T
- val check: Proof.context -> string * Position.T -> theory
+ val check: {long: bool} -> Proof.context -> string * Position.T -> theory
val axiom_table: theory -> term Name_Space.table
val axiom_space: theory -> Name_Space.T
val axioms_of: theory -> (string * term) list
@@ -132,18 +132,18 @@
let val {pos, id, ...} = rep_theory thy
in theory_markup false (Context.theory_name thy) id pos end;
-fun check ctxt (name, pos) =
+fun check long ctxt (name, pos) =
let
val thy = Proof_Context.theory_of ctxt;
val thy' =
- Context.get_theory thy name
+ Context.get_theory long thy name
handle ERROR msg =>
let
val completion =
Completion.make (name, pos)
(fn completed =>
- map Context.theory_name (ancestors_of thy)
- |> filter completed
+ map (Context.theory_name' long) (ancestors_of thy)
+ |> 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);
--- a/src/Tools/Code/code_thingol.ML Thu Jun 21 23:06:12 2018 +0100
+++ b/src/Tools/Code/code_thingol.ML Fri Jun 22 21:55:20 2018 +0200
@@ -942,6 +942,10 @@
fun read_const_exprs_internal ctxt =
let
val thy = Proof_Context.theory_of ctxt;
+ fun this_theory name =
+ if Context.theory_name thy = name then thy
+ else Context.get_theory {long = false} thy name;
+
fun consts_of thy' =
fold (fn (c, (_, NONE)) => cons c | _ => I)
(#constants (Consts.dest (Sign.consts_of thy'))) []
@@ -954,7 +958,7 @@
SOME "_" => ([], consts_of thy)
| SOME s =>
if String.isSuffix "._" s
- then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
+ then ([], consts_of_select (this_theory (unsuffix "._" s)))
else ([Code.read_const thy str], [])
| NONE => ([Code.read_const thy str], []));
in apply2 flat o split_list o map read_const_expr end;