1.1 --- a/src/HOL/IMP/Examples.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Examples.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  theory Examples imports Natural begin
     1.6  
     1.7 -constdefs
     1.8 -  factorial :: "loc => loc => com"
     1.9 -  "factorial a b == b :== (%s. 1);
    1.10 +definition
    1.11 +  factorial :: "loc => loc => com" where
    1.12 +  "factorial a b = (b :== (%s. 1);
    1.13                      \<WHILE> (%s. s a ~= 0) \<DO>
    1.14 -                    (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    1.15 +                    (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
    1.16  
    1.17  declare update_def [simp]
    1.18