src/HOL/IMPP/EvenOdd.thy

 *)
 
 EvenOdd = Misc +
 
 constdefs even :: nat => bool
-  "even n == #2 dvd n"
+  "even n == # 2 dvd n"
 
 consts
   Even, Odd :: pname
 rules 
   Even_neq_Odd "Even ~= Odd"

               Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
               Loc Res:==(%s. s<Res> * s<Arg>))"
   odd :: com
  "odd == IF (%s. s<Arg>=0)
          THEN Loc Res:==(%s. 1)
-         ELSE(Loc Res:=CALL Even (%s. s<Arg> -1))"
+         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
 
 defs
   bodies_def "bodies == [(Even,evn),(Odd,odd)]"
   
 consts