--- a/src/HOL/Modelcheck/MuCalculus.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,23 +4,26 @@
Copyright 1997 TU Muenchen
*)
-MuCalculus = Main +
+theory MuCalculus
+imports Main
+begin
types
'a pred = "'a=>bool"
-consts
-
+constdefs
Charfun :: "'a set => 'a pred"
- mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
- nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
+ "Charfun == (% A.% x. x:A)"
+
monoP :: "('a pred => 'a pred) => bool"
+ "monoP f == mono(Collect o f o Charfun)"
-defs
+ mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
+ "mu f == Charfun(lfp(Collect o f o Charfun))"
-Charfun_def "Charfun == (% A.% x. x:A)"
-monoP_def "monoP f == mono(Collect o f o Charfun)"
-mu_def "mu f == Charfun(lfp(Collect o f o Charfun))"
-nu_def "nu f == Charfun(gfp(Collect o f o Charfun))"
+ nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
+ "nu f == Charfun(gfp(Collect o f o Charfun))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end