src/HOL/IOA/ABP/Correctness.thy

   
 primrec
   reduce List.list  
   reduce_Nil  "reduce [] = []"
   reduce_Cons "reduce(x#xs) =   
-	         (case xs of   
-	             [] => [x]   
-	       |   y#ys => (if (x=y)   
-	                      then reduce xs   
-	                      else (x#(reduce xs))))"
+                 (case xs of   
+                     [] => [x]   
+               |   y#ys => (if (x=y)   
+                              then reduce xs   
+                              else (x#(reduce xs))))"
 
   
 defs
   
 system_def

 
 system_fin_def
   "system_fin_ioa == (env_ioa || impl_fin_ioa)"
   
 abs_def "abs  ==   
-	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
-	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+        (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
+         (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
 
 rules
 
   sys_IOA     "IOA system_ioa"
   sys_fin_IOA "IOA system_fin_ioa"