equal
deleted
inserted
replaced
16 chain :: "(nat=>'a::po) => bool" |
16 chain :: "(nat=>'a::po) => bool" |
17 max_in_chain :: "[nat,nat=>'a::po]=>bool" |
17 max_in_chain :: "[nat,nat=>'a::po]=>bool" |
18 finite_chain :: "(nat=>'a::po)=>bool" |
18 finite_chain :: "(nat=>'a::po)=>bool" |
19 |
19 |
20 syntax |
20 syntax |
21 |
21 "@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10) |
22 "@LUB" :: "(('b::term) => 'a) => 'a" (binder "LUB " 10) |
|
23 |
22 |
24 translations |
23 translations |
25 |
24 |
26 "LUB x. t" == "lub(range(%x. t))" |
25 "LUB x. t" == "lub(range(%x. t))" |
27 |
26 |