summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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