# HG changeset patch
# User wenzelm
# Date 1148161019 -7200
# Node ID a3a8594e19b473e59ab0c5e6a803785d1053b3cf
# Parent  877b763ded7eff989d886d68b556dc118f2e5f46
abs: precise typing;

diff -r 877b763ded7e -r a3a8594e19b4 src/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOLCF/IOA/ABP/Correctness.thy	Sat May 20 23:36:57 2006 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Sat May 20 23:36:59 2006 +0200
@@ -10,13 +10,7 @@
 begin
 
 consts
-
-reduce           :: "'a list => 'a list"
-
-abs              :: 'c
-system_ioa       :: "('m action, bool * 'm impl_state)ioa"
-system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
-
+  reduce         :: "'a list => 'a list"
 primrec
   reduce_Nil:  "reduce [] = []"
   reduce_Cons: "reduce(x#xs) =
@@ -26,18 +20,18 @@
                               then reduce xs
                               else (x#(reduce xs))))"
 
+constdefs
+  abs where
+    "abs  ==
+      (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
+       (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
 
-defs
-
-system_def:
+  system_ioa       :: "('m action, bool * 'm impl_state)ioa"
   "system_ioa == (env_ioa || impl_ioa)"
 
-system_fin_def:
+  system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
   "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))))))))))"
 
 axioms