equal
deleted
inserted
replaced
84 renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf |
84 renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf |
85 |
85 |
86 * Session HOL-Analysis: proof method "metric" implements a decision |
86 * Session HOL-Analysis: proof method "metric" implements a decision |
87 procedure for simple linear statements in metric spaces. |
87 procedure for simple linear statements in metric spaces. |
88 |
88 |
89 |
|
90 * Word: Bitwise NOT-operator has proper prefix syntax. Minor |
89 * Word: Bitwise NOT-operator has proper prefix syntax. Minor |
91 INCOMPATIBILITY. |
90 INCOMPATIBILITY. |
|
91 |
92 |
92 |
93 *** ML *** |
93 *** ML *** |
94 |
94 |
95 * Theory construction may be forked internally, the operation |
95 * Theory construction may be forked internally, the operation |
96 Theory.join_theory recovers a single result theory. See also the example |
96 Theory.join_theory recovers a single result theory. See also the example |