equal
deleted
inserted
replaced
254 for abstract algebraic reasoning using axiomatic type classes, and |
254 for abstract algebraic reasoning using axiomatic type classes, and |
255 mathematics-style proof in Isabelle/Isar; by Markus Wenzel; |
255 mathematics-style proof in Isabelle/Isar; by Markus Wenzel; |
256 |
256 |
257 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David |
257 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David |
258 von Oheimb; |
258 von Oheimb; |
|
259 |
|
260 * HOL/IMPP: extension of IMP with local variables and mutually |
|
261 recursive procedures, by David von Oheimb; |
259 |
262 |
260 * HOL/Lambda: converted into new-style theory and document; |
263 * HOL/Lambda: converted into new-style theory and document; |
261 |
264 |
262 * HOL/ex/Multiquote: example of multiple nested quotations and |
265 * HOL/ex/Multiquote: example of multiple nested quotations and |
263 anti-quotations -- basically a generalized version of de-Bruijn |
266 anti-quotations -- basically a generalized version of de-Bruijn |