src/HOL/Codegenerator_Test/Candidates.thy
changeset 59731 7fccaeec22f0
parent 59484 a130ae7a9398
child 59733 cd945dc13bec
     1.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Mar 16 15:30:00 2015 +0000
     1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 12:23:56 2015 +0000
     1.3 @@ -28,6 +28,13 @@
     1.4  
     1.5  code_pred sublist .
     1.6  
     1.7 +lemma [code]:  -- {* for the generic factorial function *}
     1.8 +  fixes XXX :: "'a :: semiring_numeral_div"
     1.9 +  shows
    1.10 +   "fact 0       = (1 :: 'a)"
    1.11 +   "fact (Suc n) = (of_nat (Suc n) * fact n :: 'a)"
    1.12 + by simp_all
    1.13 +
    1.14  code_reserved SML upto -- {* avoid popular infix *}
    1.15  
    1.16  end