--- a/src/HOL/IMP/Abs_Int0_parity.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_parity.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -114,7 +114,7 @@
 interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity is aval' and step_parity is step' and AI_parity is AI
-proof qed
+..
 
 
 subsubsection "Tests"