author wenzelm Tue, 04 Apr 2017 11:52:28 +0200 changeset 65366 10ca63a18e56 parent 65365 d32e702d7ab8 child 65367 83c30e290702
 src/HOL/Library/Combine_PER.thy file | annotate | diff | comparison | revisions src/HOL/Library/Complete_Partial_Order2.thy file | annotate | diff | comparison | revisions src/HOL/Library/Extended.thy file | annotate | diff | comparison | revisions src/HOL/Library/Multiset_Permutations.thy file | annotate | diff | comparison | revisions src/HOL/Library/Normalized_Fraction.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial_FPS.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial_Factorial.thy file | annotate | diff | comparison | revisions src/HOL/Library/Stream.thy file | annotate | diff | comparison | revisions
```--- 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

```--- a/src/HOL/Library/Stream.thy	Mon Apr 03 23:31:31 2017 +0200