summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 10 Dec 2007 11:24:12 +0100 | |

changeset 25595 | 6c48275f9c76 |

parent 25594 | 43c718438f9f |

child 25596 | ad9e3594f3f3 |

switched import from Main to List

--- 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