--- a/src/HOL/UNITY/UNITY.thy Mon May 24 15:50:23 1999 +0200
+++ b/src/HOL/UNITY/UNITY.thy Mon May 24 15:50:53 1999 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-UNITY = LessThan + Prefix +
+UNITY = LessThan + ListOrder +
typedef (Program)
@@ -37,7 +37,7 @@
"invariant A == {F. Init F <= A} Int stable A"
(*Polymorphic in both states and the meaning of <= *)
- increasing :: "['a => 'b::{ord}] => 'a program set"
+ increasing :: "['a => 'b::{order}] => 'a program set"
"increasing f == INT z. stable {s. z <= f s}"