src/HOL/IMPP/EvenOdd.ML
changeset 11464 ddea204de5bc
parent 11364 01020b10c0a7
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/IMPP/EvenOdd.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  qed "even_0";
     1.5  Addsimps [even_0];
     1.6  
     1.7 -Goalw [even_def] "even 1 = False";
     1.8 +Goalw [even_def] "even 1' = False";
     1.9  by (Simp_tac 1);
    1.10  qed "not_even_1";
    1.11  Addsimps [not_even_1];
    1.12 @@ -50,7 +50,7 @@
    1.13  
    1.14  section "verification";
    1.15  
    1.16 -Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1}. odd .{Res_ok}";
    1.17 +Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+1'}. odd .{Res_ok}";
    1.18  by (rtac hoare_derivs.If 1);
    1.19  by (rtac (hoare_derivs.Ass RS conseq1) 1);
    1.20  by  (clarsimp_tac Arg_Res_css 1);