# HG changeset patch
# User haftmann
# Date 1197282252 -3600
# Node ID 6c48275f9c7612a47554a6e867984f028960ba4e
# Parent  43c718438f9f46a69adb708e2a413a2f90dc5a90
switched import from Main to List

diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Coinductive_List.thy
--- 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 *}
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Commutative_Ring.thy
--- 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
 
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Eval_Witness.thy
--- 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 {* 
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Executable_Set.thy
--- 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 *}
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/LaTeXsugar.thy
--- 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 *)
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/List_Prefix.thy
--- 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 *}
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/List_lexord.thy
--- 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
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Multiset.thy
--- 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 *}
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Nested_Environment.thy
--- 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 {*
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/State_Monad.thy
--- 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 *}
diff -r 43c718438f9f -r 6c48275f9c76 src/HOL/Library/Word.thy
--- 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