2000-07-07 oheimb 2000-07-07 added dependency caveat
2000-07-07 oheimb 2000-07-07 added dependency caveat
2000-07-07 oheimb 2000-07-07 added IMP/Examples.ML dependence
2000-07-06 wenzelm 2000-07-06 tuned msgs;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-07-06 wenzelm 2000-07-06 Isabelle99-1;
2000-07-06 kleing 2000-07-06 ADD -> IAdd
2000-07-06 nipkow 2000-07-06 Removed some junk thms.
2000-07-06 nipkow 2000-07-06 added zabs to arith_tac
2000-07-06 nipkow 2000-07-06 Deleted list_case thms no subsumed by case_tac
2000-07-06 nipkow 2000-07-06 Now two split thms for same constant at different types is allowed.
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 bauerg 2000-07-06 removed sorry;
2000-07-06 bauerg 2000-07-06 removed sorry;
2000-07-06 kleing 2000-07-06 new ADD instruction
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 fixed typos reported by Jeremy Dawson
2000-07-06 bauerg 2000-07-06 added;
2000-07-06 bauerg 2000-07-06 completed TYPES version of HahnBanach;
2000-07-06 nipkow 2000-07-06 *** empty log message ***
2000-07-06 wenzelm 2000-07-06 Compatibility file for Moscow ML 2.00;
2000-07-06 wenzelm 2000-07-06 run Moscow ML 2.00 --- does not handle saved images (yet!?);
2000-07-06 wenzelm 2000-07-06 Moscow ML 2.00 or later (experimental!); tuned;
2000-07-05 paulson 2000-07-05 more tidying. also generalized some tactics to prove "Type A" and "a = b : A" judgements
2000-07-05 oheimb 2000-07-05 disambiguated := ; added Examples (factorial)
2000-07-05 paulson 2000-07-05 removed batch proofs
2000-07-05 paulson 2000-07-05 massive tidy-up: goal -> Goal, remove use of prems, etc.
2000-07-05 oheimb 2000-07-05 disambiguated := ; added Examples (factorial)
2000-07-05 oheimb 2000-07-05 corrected symbol for casting relation
2000-07-04 paulson 2000-07-04 removed most batch-style proofs
2000-07-04 wenzelm 2000-07-04 tuned;
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
2000-07-04 nipkow 2000-07-04 added a thm.
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
2000-07-04 oheimb 2000-07-04 added BinOp
2000-07-04 wenzelm 2000-07-04 * added 'nothing' --- the empty list of theorems;
2000-07-04 wenzelm 2000-07-04 added "nothing" (empty list of theorems);
2000-07-04 wenzelm 2000-07-04 fixed usage;
2000-07-04 wenzelm 2000-07-04 tuned comments; even smarter guessing of ProofGeneral location;
2000-07-03 wenzelm 2000-07-03 previde 'defs' field for quick_and_dirty;
2000-07-01 wenzelm 2000-07-01 IGNORE last log message! added antiquote options "long_names", "eta_contract";
2000-07-01 wenzelm 2000-07-01 removed "help";
2000-07-01 wenzelm 2000-07-01 added no_vars att;
2000-07-01 wenzelm 2000-07-01 eta_contract: no default;
2000-07-01 wenzelm 2000-07-01 GPLed;
2000-07-01 wenzelm 2000-07-01 * Isar/HOL/Calculation: new rules for substitution in inequalities (monotonicity conditions are extracted to be proven terminally);
2000-07-01 wenzelm 2000-07-01 added subst rules for ord(er), including monotonicity conditions; name all rules; tuned;
2000-07-01 wenzelm 2000-07-01 added ISABELLE_SITE_SETTINGS_PRESENT;
2000-07-01 wenzelm 2000-07-01 tuned;
2000-07-01 wenzelm 2000-07-01 added site settings check;
2000-07-01 wenzelm 2000-07-01 * Isar: removed 'help' command, which hasn't been too helpful anyway; should instead use individual commands for printing items (print_commands, print_methods etc.);
2000-07-01 wenzelm 2000-07-01 removed help; added print_commands;
2000-07-01 wenzelm 2000-07-01 removed help_methods; tuned print_methods;
2000-07-01 wenzelm 2000-07-01 removed "help"; added "print_commands", "print_trans_rules", "print_antiquotations";
2000-07-01 wenzelm 2000-07-01 added options "eta_contract", "long_names"; tuned print_antiquotations; removed help_antiquotations; tuned;
2000-07-01 wenzelm 2000-07-01 added print_trans_rules, print_antiquotations;
2000-07-01 wenzelm 2000-07-01 removed help;