2000-03-13 paulson 2000-03-13 fixed the goal statement of sorted_qsort
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-03-13 wenzelm 2000-03-13 add_thms, add_axioms, add_defs: return theorems as well;
2000-03-13 wenzelm 2000-03-13 added |>> and |>>>;
2000-03-13 nipkow 2000-03-13 exhaust->cases
2000-03-10 berghofe 2000-03-10 Type.typ_match now uses Vartab instead of association lists.
2000-03-10 paulson 2000-03-10 tidied
2000-03-10 paulson 2000-03-10 now uses recdef instead of "rules"
2000-03-10 paulson 2000-03-10 tidied, and new thm perm_append2_eq
2000-03-10 nipkow 2000-03-10 cases_tac
2000-03-10 berghofe 2000-03-10 Type.typ_match now uses Vartab instead of association lists.
2000-03-10 berghofe 2000-03-10 Type.unify now uses Vartab instead of association lists.
2000-03-10 berghofe 2000-03-10 Added function min_key.
2000-03-10 berghofe 2000-03-10 Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
2000-03-10 berghofe 2000-03-10 Envir now uses Vartab instead of association lists.
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
2000-03-10 wenzelm 2000-03-10 add_cases_induct: produce proper case names;
2000-03-10 wenzelm 2000-03-10 type descr;
2000-03-09 wenzelm 2000-03-09 check_case: disallow (T)Vars in invoked case;
2000-03-09 wenzelm 2000-03-09 quote tag arguments;
2000-03-09 wenzelm 2000-03-09 more robust case names of induct;
2000-03-09 wenzelm 2000-03-09 cleaned comment;
2000-03-09 paulson 2000-03-09 nicely tarted up Mutil
2000-03-09 wenzelm 2000-03-09 renamed to rsync-isabelle;
2000-03-09 wenzelm 2000-03-09 tuned;
2000-03-09 kleing 2000-03-09 made rsync "official"
2000-03-09 paulson 2000-03-09 mod_less, div_less are now default simprules
2000-03-09 kleing 2000-03-09 moved more lemmas to Convert (transitivity etc)
2000-03-09 paulson 2000-03-09 mod_less, div_less are now default simprules
2000-03-09 paulson 2000-03-09 Factorization
2000-03-09 kleing 2000-03-09 rsync goes "official" (started at boot time)
2000-03-09 kleing 2000-03-09 tuned for completeness of LBV
2000-03-09 kleing 2000-03-09 some more small lemmas
2000-03-09 kleing 2000-03-09 completeness of the lightweight bytecode verifier
2000-03-09 kleing 2000-03-09 added NT case for method invocation
2000-03-09 kleing 2000-03-09 minor adjustments in branch and method invocation for completeness of LBV
2000-03-09 paulson 2000-03-09 updated discussion of compilers
2000-03-08 wenzelm 2000-03-08 add_cases: omit unnamed;
2000-03-08 wenzelm 2000-03-08 invoke_case: name assumption;
2000-03-08 wenzelm 2000-03-08 fixed section syntax;
2000-03-08 wenzelm 2000-03-08 sect: exlude ":" from parser;
2000-03-08 wenzelm 2000-03-08 removed tune_names;
2000-03-08 wenzelm 2000-03-08 tuned ML types; improved translation functions; 'case' command; 'oops' command; "Emulating tactic scripts";
2000-03-08 wenzelm 2000-03-08 tuned;
2000-03-08 wenzelm 2000-03-08 added \CASE, \OBTAIN, \SORRY, \OOPS; removed \SUFF;
2000-03-08 wenzelm 2000-03-08 added dest_global/local_rules; cases/induct: tuned rule selection, always admit insts; accomodate rule case names;
2000-03-08 wenzelm 2000-03-08 mk_elims, add_cases_induct: name rule cases;
2000-03-08 wenzelm 2000-03-08 generalized FINDGOAL, HEADGOAL; handling of local contexts: method_cases, invoke_case;
2000-03-08 wenzelm 2000-03-08 handling of local contexts: print_cases, get_case, add_cases;
2000-03-08 wenzelm 2000-03-08 added METHOD_CASES, resolveq_cases_tac; removed multi_resolveq; improved 'tactic' method: bind thm(s) function;
2000-03-08 wenzelm 2000-03-08 added invoke_case;
2000-03-08 wenzelm 2000-03-08 added 'case' command; added 'print_cases' command;
2000-03-08 wenzelm 2000-03-08 added print_cases;
2000-03-08 wenzelm 2000-03-08 added 'case_names' and 'params';
2000-03-08 wenzelm 2000-03-08 added rule_cases.ML;
2000-03-08 wenzelm 2000-03-08 export ALLGOALS_RANGE;
2000-03-08 wenzelm 2000-03-08 added (un)tag_rule;
2000-03-08 wenzelm 2000-03-08 added Isar/rule_cases.ML;
2000-03-08 wenzelm 2000-03-08 added isatool mkdir; isatool document -c; isatool usedir -D -c;
2000-03-08 wenzelm 2000-03-08 isabelle -c: tell ML system to compress output image;