1998-08-05 paulson 1998-08-05 Removal of "disjoint" translation
1998-08-05 paulson 1998-08-05 New record type of programs
1998-08-05 paulson 1998-08-05 Union primitives and examples
1998-08-04 wenzelm 1998-08-04 tuned; Display.print_goals function moved to Locale.print_goals;
1998-08-04 wenzelm 1998-08-04 added LocaleGroup, PiSets examples;
1998-08-04 wenzelm 1998-08-04 added Open_locale, Close_locale; thm(s): use Locale.get_thm(s);
1998-08-04 wenzelm 1998-08-04 added 'locale' section;
1998-08-04 wenzelm 1998-08-04 Locale.setup;
1998-08-04 wenzelm 1998-08-04 added export: thm -> thm; exported print_current_goals_default; locale support;
1998-08-04 wenzelm 1998-08-04 moved print_goals to locale.ML;
1998-08-04 wenzelm 1998-08-04 added locale.ML;
1998-08-04 wenzelm 1998-08-04 added icons;
1998-08-04 paulson 1998-08-04 Renamed equals0D to equals0E
1998-08-04 paulson 1998-08-04 Renamed equals0D to equals0E; tidied
1998-08-04 paulson 1998-08-04 Constant "invariant" and new constrains_tac, ensures_tac
1998-08-04 paulson 1998-08-04 Tidying
1998-08-04 paulson 1998-08-04 Boolean quantification
1998-08-04 paulson 1998-08-04 Deleted the redundant rule mem_if
1998-08-04 wenzelm 1998-08-04 fixed disjount translation;
1998-08-04 wenzelm 1998-08-04 tuned comments;
1998-08-03 paulson 1998-08-03 Better comments
1998-08-03 paulson 1998-08-03 New rewrite rules for quantification over bounded UNIONs
1998-07-31 paulson 1998-07-31 Tidied; uses records
1998-07-31 paulson 1998-07-31 new theorems for partial funcs
1998-07-31 wenzelm 1998-07-31 Pretty.sym;
1998-07-31 wenzelm 1998-07-31 size / length: printable length;
1998-07-31 wenzelm 1998-07-31 isatool expandshort;
1998-07-31 paulson 1998-07-31 Removal of obsolete "open" commands from heads of .ML files
1998-07-31 berghofe 1998-07-31 Replaced nat.exhaustion by nat.exhaust
1998-07-31 paulson 1998-07-31 Removed HOL/IMP/Com.ML because it contained only an "open" declaration
1998-07-31 paulson 1998-07-31 tidied
1998-07-31 paulson 1998-07-31 Removal of obsolete "open" commands from heads of .ML files
1998-07-30 berghofe 1998-07-30 Fixed primrec.
1998-07-30 berghofe 1998-07-30 Fixed primrec.
1998-07-30 wenzelm 1998-07-30 made SML/NJ happy;
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-07-30 wenzelm 1998-07-30 fixed primrec;
1998-07-30 wenzelm 1998-07-30 tuned;
1998-07-30 berghofe 1998-07-30 Equations are now stored in theory.
1998-07-30 berghofe 1998-07-30 Deleted obsolete comments.
1998-07-30 berghofe 1998-07-30 Adapted to new datatype package.
1998-07-30 berghofe 1998-07-30 Script that adapts theories and proof scripts to new datatype package.
1998-07-30 wenzelm 1998-07-30 make_defs not marked as internal;
1998-07-29 wenzelm 1998-07-29 late setup of Pure and CPure;
1998-07-28 wenzelm 1998-07-28 removed global_names flag;
1998-07-28 wenzelm 1998-07-28 theory_of renamed to theory (and made public);
1998-07-28 wenzelm 1998-07-28 added Real structure (taken from SML/NJ basis lib);
1998-07-28 wenzelm 1998-07-28 tuned;
1998-07-28 paulson 1998-07-28 Tidied
1998-07-28 paulson 1998-07-28 Changed "goal" to "Goal"
1998-07-28 paulson 1998-07-28 Updated examples
1998-07-27 paulson 1998-07-27 A little quantifier duplication for IFOL
1998-07-27 paulson 1998-07-27 A few new lemmas by Mark Staples
1998-07-27 wenzelm 1998-07-27 tuned;
1998-07-27 nipkow 1998-07-27 conversion bug in simpproc list_eq
1998-07-24 wenzelm 1998-07-24 added ex/MonoidGroups (record example); moved Bin and String examples to ex;
1998-07-24 wenzelm 1998-07-24 added type and update syntax;
1998-07-24 wenzelm 1998-07-24 added more_update; added type and update syntax;
1998-07-24 nipkow 1998-07-24 update -> fun_upd
1998-07-24 nipkow 1998-07-24 Map.update -> map_upd, Unpdate.update -> fun_upd Problem: macros get confused about two updates.