author | haftmann |

Mon Dec 10 11:24:12 2007 +0100 (2007-12-10) | |

changeset 25595 | 6c48275f9c76 |

parent 25594 | 43c718438f9f |

child 25596 | ad9e3594f3f3 |

switched import from Main to List

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