--- a/src/HOL/Library/Coinductive_List.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Coinductive_List.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Potentially infinite lists as greatest fixed-point *}
theory Coinductive_List
-imports Main
+imports List
begin
subsection {* List constructors over the datatype universe *}
--- a/src/HOL/Library/Commutative_Ring.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy Mon Dec 10 11:24:12 2007 +0100
@@ -7,7 +7,7 @@
header {* Proving equalities in commutative rings *}
theory Commutative_Ring
-imports Main Parity
+imports List Parity
uses ("comm_ring.ML")
begin
--- a/src/HOL/Library/Eval_Witness.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Mon Dec 10 11:24:12 2007 +0100
@@ -7,7 +7,7 @@
header {* Evaluation Oracle with ML witnesses *}
theory Eval_Witness
-imports Main
+imports List
begin
text {*
--- a/src/HOL/Library/Executable_Set.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Executable_Set.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Implementation of finite sets by lists *}
theory Executable_Set
-imports Main
+imports List
begin
subsection {* Definitional rewrites *}
--- a/src/HOL/Library/LaTeXsugar.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
(*<*)
theory LaTeXsugar
-imports Main
+imports List
begin
(* LOGIC *)
--- a/src/HOL/Library/List_Prefix.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/List_Prefix.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* List prefixes and postfixes *}
theory List_Prefix
-imports Main
+imports List
begin
subsection {* Prefix order on lists *}
--- a/src/HOL/Library/List_lexord.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Lexicographic order on lists *}
theory List_lexord
-imports Main
+imports List
begin
instance list :: (ord) ord
--- a/src/HOL/Library/Multiset.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Multisets *}
theory Multiset
-imports Main
+imports List
begin
subsection {* The type of multisets *}
--- a/src/HOL/Library/Nested_Environment.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Nested_Environment.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Nested environments *}
theory Nested_Environment
-imports Main
+imports List
begin
text {*
--- a/src/HOL/Library/State_Monad.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/State_Monad.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Combinators syntax for generic, open state monads (single threaded monads) *}
theory State_Monad
-imports Main
+imports List
begin
subsection {* Motivation *}
--- a/src/HOL/Library/Word.thy Mon Dec 10 11:24:09 2007 +0100
+++ b/src/HOL/Library/Word.thy Mon Dec 10 11:24:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Binary Words *}
theory Word
-imports Main
+imports List
begin
subsection {* Auxilary Lemmas *}
@@ -433,10 +433,10 @@
proof (induct l1,simp_all)
fix x xs
assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
- show "\<forall>l2. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
+ show "\<forall>l2. bv_to_nat xs * 2 ^ length l2 + bitval x * 2 ^ (length xs + length l2) = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
proof
fix l2
- show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
+ show "bv_to_nat xs * 2 ^ length l2 + bitval x * 2 ^ (length xs + length l2) = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
proof -
have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
by (induct "length xs",simp_all)
@@ -445,7 +445,7 @@
by simp
also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
by (simp add: ring_distribs)
- finally show ?thesis .
+ finally show ?thesis by simp
qed
qed
qed