--- a/src/HOL/Modelcheck/MuCalculus.thy Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy Thu Aug 19 19:55:13 1999 +0200
@@ -4,10 +4,10 @@
Copyright 1997 TU Muenchen
*)
-MuCalculus = HOL + Inductive +
+MuCalculus = Main +
types
- 'a pred = "'a=>bool"
+ 'a pred = "'a=>bool"
consts
@@ -16,7 +16,7 @@
nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
monoP :: "('a pred => 'a pred) => bool"
-defs
+defs
Charfun_def "Charfun == (% A.% x. x:A)"
monoP_def "monoP f == mono(Collect o f o Charfun)"
@@ -24,5 +24,3 @@
nu_def "nu f == Charfun(gfp(Collect o f o Charfun))"
end
-
-