equal
deleted
inserted
replaced
14 BNF_Greatest_Fixpoint Filter |
14 BNF_Greatest_Fixpoint Filter |
15 Conditionally_Complete_Lattices |
15 Conditionally_Complete_Lattices |
16 Binomial |
16 Binomial |
17 GCD |
17 GCD |
18 begin |
18 begin |
19 |
|
20 text \<open> |
|
21 Classical Higher-order Logic -- only ``Main'', excluding real and |
|
22 complex numbers etc. |
|
23 \<close> |
|
24 |
19 |
25 no_notation |
20 no_notation |
26 bot ("\<bottom>") and |
21 bot ("\<bottom>") and |
27 top ("\<top>") and |
22 top ("\<top>") and |
28 inf (infixl "\<sqinter>" 70) and |
23 inf (infixl "\<sqinter>" 70) and |