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 |
|
91 INCOMPATIBILITY. |
89 |
92 |
90 *** ML *** |
93 *** ML *** |
91 |
94 |
92 * Theory construction may be forked internally, the operation |
95 * Theory construction may be forked internally, the operation |
93 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 |