# HG changeset patch
# User paulson
# Date 927553853 -7200
# Node ID 614a76ce9bc610af5da724d8a9d805d858a19014
# Parent  d1bebb7f1c50e60a96e9e3e55ffc0d28ea4cf052
increasing makes sense only for partial orderings

diff -r d1bebb7f1c50 -r 614a76ce9bc6 src/HOL/UNITY/UNITY.thy
--- 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}"