equal
deleted
inserted
replaced
115 * HOL/Auth: new protocol proofs including some for the Internet |
115 * HOL/Auth: new protocol proofs including some for the Internet |
116 protocol TLS; |
116 protocol TLS; |
117 |
117 |
118 * HOL/Map: new theory of `maps' a la VDM; |
118 * HOL/Map: new theory of `maps' a la VDM; |
119 |
119 |
|
120 * HOL/simplifier: simplification procedures nat_cancel_sums for |
|
121 cancelling out common nat summands from =, <, <= (in)equalities, or |
|
122 differences; simplification procedures nat_cancel_factor for |
|
123 cancelling common factor from =, <, <= (in)equalities over natural |
|
124 sums; nat_cancel contains both kinds of procedures; |
|
125 |
120 * HOL/simplifier: terms of the form |
126 * HOL/simplifier: terms of the form |
121 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) |
127 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) |
122 are rewritten to |
128 are rewritten to |
123 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)', |
129 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)', |
124 and those of the form |
130 and those of the form |