--- a/Admin/PLATFORMS Tue Apr 04 10:34:48 2017 +0200
+++ b/Admin/PLATFORMS Thu Apr 06 10:21:45 2017 +0200
@@ -33,11 +33,10 @@
x86-linux Ubuntu 12.04 LTS
x86_64-linux Ubuntu 12.04 LTS
- x86_64-darwin Mac OS X 10.8 Mountain Lion (macbroy30 MacBookPro6,2)
- Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1)
+ x86_64-darwin Mac OS X 10.9 Mavericks (macbroy2 MacPro4,1)
Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2)
Mac OS X 10.11 El Capitan (?)
- macOS 10.12 Sierra (?)
+ macOS 10.12 Sierra (macbroy30 MacBookPro6,2)
x86-windows Windows 7
x86_64-windows Windows 7
--- a/src/HOL/Library/Cancellation/cancel.ML Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML Thu Apr 06 10:21:45 2017 +0200
@@ -1,16 +1,9 @@
-(* Title: Provers/Arith/cancel.ML
+(* Title: HOL/Library/Cancellation/cancel.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Mathias Fleury, MPII
- Copyright 2017
-
-Based on:
- Title: Provers/Arith/cancel_numerals.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
-
-
-This simproc allows handling of types with constructors (e.g., add_mset for multisets) and iteration
-of the addition (e.g., repeat_mset for multisets).
+This simproc allows handling of types with constructors (e.g., add_mset for
+multisets) and iteration of the addition (e.g., repeat_mset for multisets).
Beware that this simproc should not compete with any more specialised especially:
- nat: the handling for Suc is more complicated than what can be done here
--- a/src/HOL/Library/Cancellation/cancel_data.ML Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Cancellation/cancel_data.ML Thu Apr 06 10:21:45 2017 +0200
@@ -1,14 +1,10 @@
-(* Title: Provers/Arith/cancel_data.ML
+(* Title: HOL/Library/Cancellation/cancel_data.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Mathias Fleury, MPII
- Copyright 2017
-
-Based on:
- Title: Tools/nat_numeral_simprocs.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Datastructure for the cancelation simprocs.
+*)
-*)
signature CANCEL_DATA =
sig
val mk_sum : typ -> term list -> term
--- a/src/HOL/Library/Cancellation/cancel_simprocs.ML Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML Thu Apr 06 10:21:45 2017 +0200
@@ -1,10 +1,6 @@
-(* Title: Provers/Arith/cancel_simprocs.ML
+(* Title: HOL/Library/Cancellation/cancel_simprocs.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Mathias Fleury, MPII
- Copyright 2017
-
-Base on:
- Title: Provers/Arith/nat_numeral_simprocs.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Cancelation simprocs declaration.
*)
--- a/src/HOL/Library/Combine_PER.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Combine_PER.thy Thu Apr 06 10:21:45 2017 +0200
@@ -3,7 +3,7 @@
section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
theory Combine_PER
- imports Main "~~/src/HOL/Library/Lattice_Syntax"
+ imports Main Lattice_Syntax
begin
definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
--- a/src/HOL/Library/Complete_Partial_Order2.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Thu Apr 06 10:21:45 2017 +0200
@@ -5,8 +5,7 @@
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
- Main
- "~~/src/HOL/Library/Lattice_Syntax"
+ Main Lattice_Syntax
begin
lemma chain_transfer [transfer_rule]:
--- a/src/HOL/Library/Extended.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Extended.thy Thu Apr 06 10:21:45 2017 +0200
@@ -5,9 +5,7 @@
*)
theory Extended
-imports
- Main
- "~~/src/HOL/Library/Simps_Case_Conv"
+ imports Simps_Case_Conv
begin
datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
--- a/src/HOL/Library/Multiset_Permutations.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Multiset_Permutations.thy Thu Apr 06 10:21:45 2017 +0200
@@ -1,16 +1,17 @@
-(*
- File: Multiset_Permutations.thy
- Author: Manuel Eberl (TU München)
+(* Title: HOL/Library/Multiset_Permutations.thy
+ Author: Manuel Eberl (TU München)
- Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose
- entries correspond to the multiset (resp. set).
+Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose
+entries correspond to the multiset (resp. set).
*)
+
section \<open>Permutations of a Multiset\<close>
+
theory Multiset_Permutations
imports
Complex_Main
- "~~/src/HOL/Library/Multiset"
- "~~/src/HOL/Library/Permutations"
+ Multiset
+ Permutations
begin
(* TODO Move *)
--- a/src/HOL/Library/Normalized_Fraction.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Normalized_Fraction.thy Thu Apr 06 10:21:45 2017 +0200
@@ -6,7 +6,7 @@
imports
Main
"~~/src/HOL/Number_Theory/Euclidean_Algorithm"
- "~~/src/HOL/Library/Fraction_Field"
+ Fraction_Field
begin
definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
--- a/src/HOL/Library/Polynomial.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Polynomial.thy Thu Apr 06 10:21:45 2017 +0200
@@ -10,8 +10,8 @@
theory Polynomial
imports
"~~/src/HOL/Deriv"
- "~~/src/HOL/Library/More_List"
- "~~/src/HOL/Library/Infinite_Set"
+ More_List
+ Infinite_Set
begin
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
--- a/src/HOL/Library/Polynomial_FPS.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Thu Apr 06 10:21:45 2017 +0200
@@ -1,13 +1,13 @@
-(*
- File: Polynomial_FPS.thy
- Author: Manuel Eberl (TUM)
+(* Title: HOL/Library/Polynomial_FPS.thy
+ Author: Manuel Eberl, TU München
- Converting polynomials to formal power series
+Converting polynomials to formal power series.
*)
section \<open>Converting polynomials to formal power series\<close>
+
theory Polynomial_FPS
-imports Polynomial Formal_Power_Series
+ imports Polynomial Formal_Power_Series
begin
definition fps_of_poly where
--- a/src/HOL/Library/Polynomial_Factorial.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Thu Apr 06 10:21:45 2017 +0200
@@ -9,9 +9,9 @@
theory Polynomial_Factorial
imports
Complex_Main
- "~~/src/HOL/Library/Polynomial"
- "~~/src/HOL/Library/Normalized_Fraction"
- "~~/src/HOL/Library/Field_as_Ring"
+ Polynomial
+ Normalized_Fraction
+ Field_as_Ring
begin
subsection \<open>Various facts about polynomials\<close>
--- a/src/HOL/Library/Stream.thy Tue Apr 04 10:34:48 2017 +0200
+++ b/src/HOL/Library/Stream.thy Thu Apr 06 10:21:45 2017 +0200
@@ -9,7 +9,7 @@
section \<open>Infinite Streams\<close>
theory Stream
-imports "~~/src/HOL/Library/Nat_Bijection"
+ imports Nat_Bijection
begin
codatatype (sset: 'a) stream =
--- a/src/Pure/PIDE/resources.scala Tue Apr 04 10:34:48 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Thu Apr 06 10:21:45 2017 +0200
@@ -80,15 +80,12 @@
def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
{
val theory = Thy_Header.base_name(s)
- val is_base_name = Thy_Header.is_base_name(s)
- val is_qualified = is_base_name && Long_Name.is_qualified(s)
+ val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
val known_theory =
- if (is_base_name)
- session_base.known_theories.get(theory) orElse
- (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
- else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
- else None
+ session_base.known_theories.get(theory) orElse
+ (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
+ else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
known_theory match {
case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
--- a/src/Pure/Tools/spell_checker.scala Tue Apr 04 10:34:48 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala Thu Apr 06 10:21:45 2017 +0200
@@ -1,4 +1,4 @@
-/* Title: Tools/jEdit/src/spell_checker.scala
+/* Title: Pure/Tools/spell_checker.scala
Author: Makarius
Spell checker with completion, based on JOrtho (see
--- a/src/Tools/VSCode/src/build_vscode.scala Tue Apr 04 10:34:48 2017 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala Thu Apr 06 10:21:45 2017 +0200
@@ -1,4 +1,4 @@
-/* Title: Pure/Admin/build_vscode.scala
+/* Title: Tools/VSCode/src/build_vscode.scala
Author: Makarius
Build VSCode configuration and extension module for Isabelle.