diff -r 2b8c2a7547ab -r 21eb5e156d91 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Tue Feb 06 12:27:17 1996 +0100 +++ b/src/HOLCF/Porder.thy Tue Feb 06 12:42:31 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOLCF/porder.thy +(* Title: HOLCF/porder.thy ID: \$Id\$ - Author: Franz Regensburger + Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Conservative extension of theory Porder0 by constant definitions @@ -9,28 +9,28 @@ Porder = Porder0 + -consts - "<|" :: "['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" - max_in_chain :: "[nat,nat=>'a::po]=>bool" - finite_chain :: "(nat=>'a::po)=>bool" +consts + "<|" :: "['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" + max_in_chain :: "[nat,nat=>'a::po]=>bool" + finite_chain :: "(nat=>'a::po)=>bool" defs (* class definitions *) -is_ub "S <| x == ! y.y:S --> y< x << u)" +is_ub "S <| x == ! y.y:S --> y< x << u)" (* Arbitrary chains are total orders *) -is_tord "is_tord(S) == ! x y. x:S & y:S --> (x< (x<