src/HOL/IMPP/EvenOdd.ML
changeset 17477 ceb42ea2f223
parent 15354 9234f5765d9c
     1.1 --- a/src/HOL/IMPP/EvenOdd.ML	Sat Sep 17 19:17:35 2005 +0200
     1.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Sat Sep 17 20:14:30 2005 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Copyright   1999 TUM
     1.5  *)
     1.6  
     1.7 -section "even"; 
     1.8 +section "even";
     1.9  
    1.10  Goalw [even_def] "even 0";
    1.11  by (Simp_tac 1);
    1.12 @@ -71,14 +71,14 @@
    1.13  by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
    1.14  by (rtac export_s 1);
    1.15  by  (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
    1.16 -		   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
    1.17 +                   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
    1.18  by (rtac (single_asm RS conseq2) 1);
    1.19  by   (clarsimp_tac Arg_Res_css 1);
    1.20  by  (force_tac Arg_Res_css 1);
    1.21  by (rtac export_s 1);
    1.22  by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
    1.23 -		  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
    1.24 -		 (Call_invariant RS conseq12) 1);
    1.25 +                  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
    1.26 +                 (Call_invariant RS conseq12) 1);
    1.27  by (rtac (single_asm RS conseq2) 1);
    1.28  by  (clarsimp_tac Arg_Res_css 1);
    1.29  by (force_tac Arg_Res_css 1);
    1.30 @@ -97,7 +97,7 @@
    1.31  
    1.32  Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
    1.33  by (rtac conseq1 1);
    1.34 -by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), 
    1.35 +by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"),
    1.36        ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
    1.37        ("Q","%pn. Res_ok")] Body1 1);
    1.38  by    Auto_tac;