Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IOA/ABP/Correctness.thy
changeset 1476 608483c2122a
parent 1376 92f83b9d17e1 
--- a/src/HOL/IOA/ABP/Correctness.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -20,11 +20,11 @@
   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
@@ -36,8 +36,8 @@
   "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
isabelle