summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 04 Apr 2017 11:52:28 +0200 | |

changeset 65366 | 10ca63a18e56 |

parent 65365 | d32e702d7ab8 |

child 65367 | 83c30e290702 |

proper imports;
tuned headers;

--- a/src/HOL/Library/Combine_PER.thy Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Combine_PER.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Complete_Partial_Order2.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Extended.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Multiset_Permutations.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Normalized_Fraction.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Polynomial.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Polynomial_FPS.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Tue Apr 04 11:52:28 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 Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Stream.thy Tue Apr 04 11:52:28 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 =