src/HOL/MicroJava/J/TypeRel.thy
changeset 32461 eee4fa79398f
parent 28562 4e74209f113e
child 33954 1bc3b688548c
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Aug 31 17:32:29 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Aug 31 20:32:00 2009 +0200
     1.3 @@ -97,6 +97,14 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +text {* Code generator setup (FIXME!) *}
     1.8 +
     1.9 +consts_code
    1.10 +  "wfrec"   ("\<module>wfrec?")
    1.11 +attach {*
    1.12 +fun wfrec f x = f (wfrec f) x;
    1.13 +*}
    1.14 +
    1.15  consts
    1.16  
    1.17    method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)