summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Tue, 05 Mar 2002 18:54:55 +0100 | |

changeset 13023 | f869b6822006 |

parent 13022 | b115b305612f |

child 13024 | 0461b281c2b5 |

Added two paragraphs on "rules" method and code generator.

--- a/NEWS Tue Mar 05 18:19:11 2002 +0100 +++ b/NEWS Tue Mar 05 18:54:55 2002 +0100 @@ -151,6 +151,10 @@ text; the fixed correlation with particular command syntax has been discontinued; +* Pure: new method 'rules' is particularly well-suited for proof +search in intuitionistic logic; a bit slower than 'blast' or 'fast', +but often produces more compact proof terms with less detours; + * Pure/Provers/classical: simplified integration with pure rule attributes and methods; the classical "intro?/elim?/dest?" declarations coincide with the pure ones; the "rule" method no longer @@ -233,6 +237,11 @@ - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype; +* HOL: generic code generator for generating executable ML code from +specifications; specific support for HOL constructs such as inductive +datatypes and sets, as well as recursive functions; can be invoked +via 'generate_code' theory section; + * HOL: canonical cases/induct rules for n-tuples (n = 3..7); * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"