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

author | paulson |

Thu, 07 Jan 1999 11:08:29 +0100 | |

changeset 6069 | a99879bd9f13 |

parent 6068 | 2d8f3e1f1151 |

child 6070 | 032babd0120b |

if-then-else syntax for ZF

--- a/NEWS Thu Jan 07 10:56:05 1999 +0100 +++ b/NEWS Thu Jan 07 11:08:29 1999 +0100 @@ -12,6 +12,14 @@ constants declared in the same theory; +*** Proof tools *** + +* Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision +procedure for linear arithmetic. Currently it is used for types `nat' and +`int' in HOL (see below) but can, should and will be instantiated for other +types and logics as well. + + *** General *** * in locales, the "assumes" and "defines" parts may be omitted if empty; @@ -60,6 +68,8 @@ * the datatype declaration of type T now defines the recursor T_rec; +* The syntax "if P then x else y" is now available in addition to if(P,x,y). + New in Isabelle98-1 (October 1998) ----------------------------------