added code_constsubst
authorhaftmann
Tue Oct 10 09:17:19 2006 +0200 (2006-10-10)
changeset 209333f999b73f6d5
parent 20932 e65e1234c9d3
child 20934 2b872c161747
added code_constsubst
src/HOL/Extraction/Pigeonhole.thy
     1.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 10 09:17:18 2006 +0200
     1.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Tue Oct 10 09:17:19 2006 +0200
     1.3 @@ -304,14 +304,16 @@
     1.4  definition
     1.5    arbitrary_nat :: "nat \<times> nat"
     1.6    "arbitrary_nat = arbitrary"
     1.7 +  arbitrary_nat_subst :: "nat \<times> nat"
     1.8 +  "arbitrary_nat_subst = (0, 0)"
     1.9  
    1.10  lemma [code func]:
    1.11    "arbitrary_nat = arbitrary_nat" ..
    1.12  
    1.13  declare arbitrary_nat_def [symmetric, code inline]
    1.14  
    1.15 -code_const arbitrary_nat
    1.16 -  (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
    1.17 +code_constsubst
    1.18 +  arbitrary_nat \<equiv> arbitrary_nat_subst
    1.19  
    1.20  definition
    1.21    "test n = pigeonhole n (\<lambda>m. m - 1)"