equal
deleted
inserted
replaced
158 |
158 |
159 * IsaMakefile: the HOL-Real target now builds an actual image; |
159 * IsaMakefile: the HOL-Real target now builds an actual image; |
160 |
160 |
161 |
161 |
162 ** HOL misc ** |
162 ** HOL misc ** |
|
163 |
|
164 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces |
|
165 (in Isabelle/Isar) -- by Gertrud Bauer; |
163 |
166 |
164 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
167 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
165 -- avoids syntactic ambiguities and treats state, transition, and |
168 -- avoids syntactic ambiguities and treats state, transition, and |
166 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
169 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
167 changed syntax and (many) tactics; |
170 changed syntax and (many) tactics; |