1998-08-06 nipkow 1998-08-06 *** empty log message ***
1998-08-06 nipkow 1998-08-06 Lemma renamed in HOL.
1998-08-06 nipkow 1998-08-06 Added macro `termi'
1998-08-06 nipkow 1998-08-06 New lemmas in List and Lambda in IsaMakefile
1998-08-06 nipkow 1998-08-06 Removed duplicate thms (see comment to Arith.ML)
1998-08-06 nipkow 1998-08-06 Removed duplicate thms: less_imp_add_less = trans_less_add1 le_imp_add_le = trans_le_add1
1998-08-06 nipkow 1998-08-06 Removed comments.
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 disjointness
1998-08-06 paulson 1998-08-06 Now recognizes both {}= and ={}
1998-08-06 paulson 1998-08-06 Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying)
1998-08-06 paulson 1998-08-06 New result from AC directory
1998-08-06 wenzelm 1998-08-06 added solve_tac;
1998-08-06 paulson 1998-08-06 New results from AC
1998-08-06 nipkow 1998-08-06 First steps towards termination of simply typed terms.
1998-08-06 wenzelm 1998-08-06 binding / skolem vars;
1998-08-05 paulson 1998-08-05 Null program and a few new results
1998-08-05 paulson 1998-08-05 Finished the example
1998-08-05 paulson 1998-08-05 Indentation, comments
1998-08-05 paulson 1998-08-05 Renamed equals0D to equals0E
1998-08-05 paulson 1998-08-05 Tidied
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.