diff -r c1b83b42f65a -r c8a8482a8124 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/Porder.thy	Tue Mar 10 18:33:13 1998 +0100
@@ -13,8 +13,8 @@
         "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)
         "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)
         lub     ::      "'a set => 'a::po"
-        is_tord ::      "'a::po set => bool"
-        is_chain ::     "(nat=>'a::po) => bool"
+        tord ::      "'a::po set => bool"
+        chain ::     "(nat=>'a::po) => bool"
         max_in_chain :: "[nat,nat=>'a::po]=>bool"
         finite_chain :: "(nat=>'a::po)=>bool"
 
@@ -37,14 +37,14 @@
 is_lub          "S <<| x == S <| x & (! u. S <| u  --> x << u)"
 
 (* Arbitrary chains are total orders    *)                  
-is_tord         "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
+tord         "tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
 
 (* Here we use countable chains and I prefer to code them as functions! *)
-is_chain        "is_chain F == (! i. F(i) << F(Suc(i)))"
+chain        "chain F == (! i. F(i) << F(Suc(i)))"
 
 (* finite chains, needed for monotony of continouous functions *)
 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
-finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
+finite_chain_def "finite_chain C == chain(C) & (? i. max_in_chain i C)"
 
 lub_def          "lub S == (@x. S <<| x)"