The function package declares the [code] attribute automatically again.
authorkrauss
Fri Nov 24 13:43:44 2006 +0100 (2006-11-24)
changeset 2151116c62deb1adf
parent 21510 7e72185e4b24
child 21512 3786eb1b69d6
The function package declares the [code] attribute automatically again.
src/HOL/Library/ExecutableSet.thy
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/Library/ExecutableSet.thy	Fri Nov 24 13:39:22 2006 +0100
     1.2 +++ b/src/HOL/Library/ExecutableSet.thy	Fri Nov 24 13:43:44 2006 +0100
     1.3 @@ -125,7 +125,6 @@
     1.4  termination by lexicographic_order
     1.5  
     1.6  lemmas unionl_def = unionl.simps(2)
     1.7 -declare unionl.simps[code]
     1.8  
     1.9  function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.10  where
    1.11 @@ -136,7 +135,6 @@
    1.12  termination by lexicographic_order
    1.13  
    1.14  lemmas intersect_def = intersect.simps(3)
    1.15 -declare intersect.simps[code]
    1.16  
    1.17  function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.18  where
    1.19 @@ -147,7 +145,6 @@
    1.20  termination by lexicographic_order
    1.21  
    1.22  lemmas subtract_def = subtract.simps(3)
    1.23 -declare subtract.simps[code]
    1.24  
    1.25  function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
    1.26  where
    1.27 @@ -157,7 +154,6 @@
    1.28  termination by lexicographic_order
    1.29  
    1.30  lemmas map_distinct_def = map_distinct.simps(2)
    1.31 -declare map_distinct.simps[code]
    1.32  
    1.33  function unions :: "'a list list \<Rightarrow> 'a list"
    1.34  where
    1.35 @@ -167,7 +163,6 @@
    1.36  termination by lexicographic_order
    1.37  
    1.38  lemmas unions_def = unions.simps(2)
    1.39 -declare unions.simps[code]
    1.40  
    1.41  consts intersects :: "'a list list \<Rightarrow> 'a list"
    1.42  primrec
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Nov 24 13:39:22 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Nov 24 13:43:44 2006 +0100
     2.3 @@ -142,15 +142,15 @@
     2.4        val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
     2.5        val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
     2.6  
     2.7 -        (* FIXME: How to generate code from (possibly) local contexts
     2.8 -        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
     2.9 -        val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    2.10 -        *)
    2.11 -        val qualify = NameSpace.qualified defname;
    2.12 +        (* FIXME: How to generate code from (possibly) local contexts*)
    2.13 +      val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    2.14 +      val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    2.15 +        
    2.16 +      val qualify = NameSpace.qualified defname;
    2.17      in
    2.18 -        lthy
    2.19 -          |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
    2.20 -          |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
    2.21 +      lthy
    2.22 +        |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
    2.23 +        |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
    2.24      end
    2.25  
    2.26  
     3.1 --- a/src/HOL/ex/Codegenerator.thy	Fri Nov 24 13:39:22 2006 +0100
     3.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Nov 24 13:43:44 2006 +0100
     3.3 @@ -54,8 +54,6 @@
     3.4    by pat_completeness auto
     3.5  termination by (relation "measure nat") auto
     3.6  
     3.7 -declare fac.simps [code]
     3.8 -
     3.9  subsection {* sums *}
    3.10  
    3.11  subsection {* options *}