diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
index 732b9d89f7c96e70bc045efe99dac7d0b04a2c93..e39b0249ab2b9e3cd8043eb752c0e09de36f0986 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_CAS.thy
@@ -283,7 +283,7 @@ lemma aux9[simp]:
   using not_less_eq_eq by force
 
 
-
+ 
 
 theorem (in is_prime) is_prime_correct':
     "\<lbrace> \<lambda>\<sigma>. n \<le> UINT_MAX \<rbrace> is_prime' n \<lbrace> \<lambda>res \<sigma>. (res \<noteq> 0) \<longleftrightarrow> prime n \<rbrace>!"
@@ -343,7 +343,6 @@ method annotate_loops for n::nat = (prep, subst whileLoopE_invL1[of _ n])
                                    (* this must be generalized for several loops *)
 
 
-
 (* and now the scheme for an automated proof, provided that sufficient
    background knowledge had been inserted into the prover 'auto'. *)
 
@@ -361,4 +360,27 @@ theorem (in is_prime) is_prime_correct''':
    by    (wp, auto )  
 
 
+(* yet another way with Frederics stuff *)
+
+method vcg = (subst is_prime.is_prime'_annot,prep, wp)
+
+thm is_prime.is_prime'_annot
+
+context is_prime 
+begin
+
+definition [prog_annotations]:"requires = is_prime_requires"
+definition [prog_annotations]:"ensures  = is_prime_ensures"
+
+
+
+theorem is_prime_correct'''': 
+  "\<lbrace>requires n\<rbrace> is_prime' n \<lbrace>ensures n\<rbrace>!" 
+  by(vcg, auto)  
+
+
+
+end
+
+
 end