# HG changeset patch # User eberlm # Date 1491466905 -7200 # Node ID 3f291f7a36460f16f7ed889ef0cdaa977f36fccd # Parent 27c1b5e952bdd9d15c3b0cc140418fa076ce439e# Parent a14fa655b48c9231eb6957d52d923416b2c01eeb Merged diff -r a14fa655b48c -r 3f291f7a3646 Admin/PLATFORMS --- 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 diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Cancellation/cancel.ML --- 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 diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Cancellation/cancel_data.ML --- 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 diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Cancellation/cancel_simprocs.ML --- 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. *) diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Combine_PER.thy --- 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 \A combinator to build partial equivalence relations from a predicate and an equivalence relation\ theory Combine_PER - imports Main "~~/src/HOL/Library/Lattice_Syntax" + imports Main Lattice_Syntax begin definition combine_per :: "('a \ bool) \ ('a \ 'a \ bool) \ 'a \ 'a \ bool" diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Complete_Partial_Order2.thy --- 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 \Formalisation of chain-complete partial orders, continuity and admissibility\ theory Complete_Partial_Order2 imports - Main - "~~/src/HOL/Library/Lattice_Syntax" + Main Lattice_Syntax begin lemma chain_transfer [transfer_rule]: diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Extended.thy --- 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 ("\") | Minf ("-\") diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Multiset_Permutations.thy --- 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 \Permutations of a Multiset\ + theory Multiset_Permutations imports Complex_Main - "~~/src/HOL/Library/Multiset" - "~~/src/HOL/Library/Permutations" + Multiset + Permutations begin (* TODO Move *) diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Normalized_Fraction.thy --- 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} \ 'a \ 'a fract" where diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Polynomial.thy --- 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 \Auxiliary: operations for lists (later) representing coefficients\ diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Polynomial_FPS.thy --- 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 \Converting polynomials to formal power series\ + theory Polynomial_FPS -imports Polynomial Formal_Power_Series + imports Polynomial Formal_Power_Series begin definition fps_of_poly where diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Polynomial_Factorial.thy --- 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 \Various facts about polynomials\ diff -r a14fa655b48c -r 3f291f7a3646 src/HOL/Library/Stream.thy --- 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 \Infinite Streams\ theory Stream -imports "~~/src/HOL/Library/Nat_Bijection" + imports Nat_Bijection begin codatatype (sset: 'a) stream = diff -r a14fa655b48c -r 3f291f7a3646 src/Pure/PIDE/resources.scala --- 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) diff -r a14fa655b48c -r 3f291f7a3646 src/Pure/Tools/spell_checker.scala --- 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 diff -r a14fa655b48c -r 3f291f7a3646 src/Tools/VSCode/src/build_vscode.scala --- 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.