1.1 --- a/src/HOL/IMPP/EvenOdd.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -10,38 +10,41 @@
     1.4  imports Misc
     1.5  begin
     1.6  
     1.7 -constdefs
     1.8 -  even :: "nat => bool"
     1.9 -  "even n == 2 dvd n"
    1.10 +definition
    1.11 +  even :: "nat => bool" where
    1.12 +  "even n = (2 dvd n)"
    1.13  
    1.14 -consts
    1.15 -  Even :: pname
    1.16 +axiomatization
    1.17 +  Even :: pname and
    1.18    Odd :: pname
    1.19 -axioms
    1.20 -  Even_neq_Odd: "Even ~= Odd"
    1.21 +where
    1.22 +  Even_neq_Odd: "Even ~= Odd" and
    1.23    Arg_neq_Res:  "Arg  ~= Res"
    1.24  
    1.25 -constdefs
    1.26 -  evn :: com
    1.27 - "evn == IF (%s. s<Arg> = 0)
    1.28 +definition
    1.29 +  evn :: com where
    1.30 + "evn = (IF (%s. s<Arg> = 0)
    1.31           THEN Loc Res:==(%s. 0)
    1.32           ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
    1.33                Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
    1.34 -              Loc Res:==(%s. s<Res> * s<Arg>))"
    1.35 -  odd :: com
    1.36 - "odd == IF (%s. s<Arg> = 0)
    1.37 +              Loc Res:==(%s. s<Res> * s<Arg>)))"
    1.38 +
    1.39 +definition
    1.40 +  odd :: com where
    1.41 + "odd = (IF (%s. s<Arg> = 0)
    1.42           THEN Loc Res:==(%s. 1)
    1.43 -         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
    1.44 +         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
    1.45  
    1.46  defs
    1.47    bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
    1.48  
    1.49 -consts
    1.50 -  Z_eq_Arg_plus   :: "nat => nat assn" ("Z=Arg+_" [50]50)
    1.51 - "even_Z=(Res=0)" ::        "nat assn" ("Res'_ok")
    1.52 -defs
    1.53 -  Z_eq_Arg_plus_def: "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
    1.54 -  Res_ok_def:       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
    1.55 +definition
    1.56 +  Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
    1.57 +  "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
    1.58 +
    1.59 +definition
    1.60 +  Res_ok :: "nat assn" where
    1.61 +  "Res_ok = (%Z s. even Z = (s<Res> = 0))"
    1.62  
    1.63  
    1.64  subsection "even"