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

author | wenzelm |

Tue, 14 Mar 2006 16:29:29 +0100 | |

changeset 19254 | efaf5d47049e |

parent 19253 | f3ce97b5661a |

child 19255 | e80e3fdda606 |

Pure: no_translations;

--- a/NEWS Tue Mar 14 14:25:09 2006 +0100 +++ b/NEWS Tue Mar 14 16:29:29 2006 +0100 @@ -34,6 +34,9 @@ *** Pure *** +* Command 'no_translations' removes translation rules from theory +syntax. + * Isar: improper proof element 'guess' is like 'obtain', but derives the obtained context from the course of reasoning! For example: @@ -390,9 +393,10 @@ * Library: added theory Coinductive_List of potentially infinite lists as greatest fixed-point. -* Library: added theory AssocList which implements (finite) maps as +* Library: added theory AssocList which implements (finite) maps as association lists. + *** ML *** * Pure/library: