dropped superfluous code lemmas
authorhaftmann
Tue Sep 16 09:21:26 2008 +0200 (2008-09-16)
changeset 282294f06fae6a55e
parent 28228 7ebe8dc06cbb
child 28230 87feb146d3d1
dropped superfluous code lemmas
src/HOL/Equiv_Relations.thy
src/HOL/Library/Word.thy
src/HOL/NatBin.thy
src/HOL/ex/ExecutableContent.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Tue Sep 16 09:21:24 2008 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Tue Sep 16 09:21:26 2008 +0200
     1.3 @@ -93,9 +93,8 @@
     1.4  
     1.5  subsection {* Quotients *}
     1.6  
     1.7 -constdefs
     1.8 -  quotient :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/'/" 90)
     1.9 -  "A//r == \<Union>x \<in> A. {r``{x}}"  -- {* set of equiv classes *}
    1.10 +definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90) where
    1.11 +  [code func del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
    1.12  
    1.13  lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
    1.14    by (unfold quotient_def) blast
     2.1 --- a/src/HOL/Library/Word.thy	Tue Sep 16 09:21:24 2008 +0200
     2.2 +++ b/src/HOL/Library/Word.thy	Tue Sep 16 09:21:26 2008 +0200
     2.3 @@ -2267,6 +2267,8 @@
     2.4    fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
     2.5      fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
     2.6  
     2.7 +declare fast_bv_to_nat_helper.simps [code func del]
     2.8 +
     2.9  lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
    2.10      fast_bv_to_nat_helper bs (Int.Bit0 bin)"
    2.11    by simp
     3.1 --- a/src/HOL/NatBin.thy	Tue Sep 16 09:21:24 2008 +0200
     3.2 +++ b/src/HOL/NatBin.thy	Tue Sep 16 09:21:26 2008 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4  begin
     3.5  
     3.6  definition
     3.7 -  nat_number_of_def [code inline]: "number_of v = nat (number_of v)"
     3.8 +  nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)"
     3.9  
    3.10  instance ..
    3.11  
     4.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Sep 16 09:21:24 2008 +0200
     4.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue Sep 16 09:21:26 2008 +0200
     4.3 @@ -11,7 +11,6 @@
     4.4    Binomial
     4.5    Commutative_Ring
     4.6    Enum
     4.7 -  Eval
     4.8    List_Prefix
     4.9    Nat_Infinity
    4.10    Nested_Environment
    4.11 @@ -20,19 +19,10 @@
    4.12    Primes
    4.13    Product_ord
    4.14    SetsAndFunctions
    4.15 -  State_Monad
    4.16    While_Combinator
    4.17    Word
    4.18    "~~/src/HOL/ex/Commutative_Ring_Complete"
    4.19    "~~/src/HOL/ex/Records"
    4.20  begin
    4.21  
    4.22 -lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
    4.23 -declare fast_bv_to_nat_helper.simps [code func del]
    4.24 -
    4.25 -setup {*
    4.26 -  Code.del_funcs
    4.27 -    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
    4.28 -*}
    4.29 -
    4.30  end