switched import from Main to List
authorhaftmann
Mon Dec 10 11:24:12 2007 +0100 (2007-12-10)
changeset 255956c48275f9c76
parent 25594 43c718438f9f
child 25596 ad9e3594f3f3
switched import from Main to List
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Word.thy
     1.1 --- a/src/HOL/Library/Coinductive_List.thy	Mon Dec 10 11:24:09 2007 +0100
     1.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Dec 10 11:24:12 2007 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Potentially infinite lists as greatest fixed-point *}
     1.5  
     1.6  theory Coinductive_List
     1.7 -imports Main
     1.8 +imports List
     1.9  begin
    1.10  
    1.11  subsection {* List constructors over the datatype universe *}
     2.1 --- a/src/HOL/Library/Commutative_Ring.thy	Mon Dec 10 11:24:09 2007 +0100
     2.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Mon Dec 10 11:24:12 2007 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Proving equalities in commutative rings *}
     2.5  
     2.6  theory Commutative_Ring
     2.7 -imports Main Parity
     2.8 +imports List Parity
     2.9  uses ("comm_ring.ML")
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Library/Eval_Witness.thy	Mon Dec 10 11:24:09 2007 +0100
     3.2 +++ b/src/HOL/Library/Eval_Witness.thy	Mon Dec 10 11:24:12 2007 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  header {* Evaluation Oracle with ML witnesses *}
     3.5  
     3.6  theory Eval_Witness
     3.7 -imports Main
     3.8 +imports List
     3.9  begin
    3.10  
    3.11  text {* 
     4.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Dec 10 11:24:09 2007 +0100
     4.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Dec 10 11:24:12 2007 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Implementation of finite sets by lists *}
     4.5  
     4.6  theory Executable_Set
     4.7 -imports Main
     4.8 +imports List
     4.9  begin
    4.10  
    4.11  subsection {* Definitional rewrites *}
     5.1 --- a/src/HOL/Library/LaTeXsugar.thy	Mon Dec 10 11:24:09 2007 +0100
     5.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Dec 10 11:24:12 2007 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  (*<*)
     5.6  theory LaTeXsugar
     5.7 -imports Main
     5.8 +imports List
     5.9  begin
    5.10  
    5.11  (* LOGIC *)
     6.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Dec 10 11:24:09 2007 +0100
     6.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Dec 10 11:24:12 2007 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* List prefixes and postfixes *}
     6.5  
     6.6  theory List_Prefix
     6.7 -imports Main
     6.8 +imports List
     6.9  begin
    6.10  
    6.11  subsection {* Prefix order on lists *}
     7.1 --- a/src/HOL/Library/List_lexord.thy	Mon Dec 10 11:24:09 2007 +0100
     7.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Dec 10 11:24:12 2007 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* Lexicographic order on lists *}
     7.5  
     7.6  theory List_lexord
     7.7 -imports Main
     7.8 +imports List
     7.9  begin
    7.10  
    7.11  instance list :: (ord) ord
     8.1 --- a/src/HOL/Library/Multiset.thy	Mon Dec 10 11:24:09 2007 +0100
     8.2 +++ b/src/HOL/Library/Multiset.thy	Mon Dec 10 11:24:12 2007 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* Multisets *}
     8.5  
     8.6  theory Multiset
     8.7 -imports Main
     8.8 +imports List
     8.9  begin
    8.10  
    8.11  subsection {* The type of multisets *}
     9.1 --- a/src/HOL/Library/Nested_Environment.thy	Mon Dec 10 11:24:09 2007 +0100
     9.2 +++ b/src/HOL/Library/Nested_Environment.thy	Mon Dec 10 11:24:12 2007 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Nested environments *}
     9.5  
     9.6  theory Nested_Environment
     9.7 -imports Main
     9.8 +imports List
     9.9  begin
    9.10  
    9.11  text {*
    10.1 --- a/src/HOL/Library/State_Monad.thy	Mon Dec 10 11:24:09 2007 +0100
    10.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Dec 10 11:24:12 2007 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Combinators syntax for generic, open state monads (single threaded monads) *}
    10.5  
    10.6  theory State_Monad
    10.7 -imports Main
    10.8 +imports List
    10.9  begin
   10.10  
   10.11  subsection {* Motivation *}
    11.1 --- a/src/HOL/Library/Word.thy	Mon Dec 10 11:24:09 2007 +0100
    11.2 +++ b/src/HOL/Library/Word.thy	Mon Dec 10 11:24:12 2007 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Binary Words *}
    11.5  
    11.6  theory Word
    11.7 -imports Main
    11.8 +imports List
    11.9  begin
   11.10  
   11.11  subsection {* Auxilary Lemmas *}
   11.12 @@ -433,10 +433,10 @@
   11.13    proof (induct l1,simp_all)
   11.14      fix x xs
   11.15      assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
   11.16 -    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"
   11.17 +    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"
   11.18      proof
   11.19        fix l2
   11.20 -      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"
   11.21 +      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"
   11.22        proof -
   11.23          have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
   11.24            by (induct "length xs",simp_all)
   11.25 @@ -445,7 +445,7 @@
   11.26            by simp
   11.27          also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   11.28            by (simp add: ring_distribs)
   11.29 -        finally show ?thesis .
   11.30 +        finally show ?thesis by simp
   11.31        qed
   11.32      qed
   11.33    qed