2000-09-14 nipkow 2000-09-14 *** empty log message ***
2000-09-14 nipkow 2000-09-14 *** empty log message ***
2000-09-14 wenzelm 2000-09-14 added /usr/share/emacs/ProofGeneral/isar/interface choice;
2000-09-14 paulson 2000-09-14 a bit more of division
2000-09-13 wenzelm 2000-09-13 dummy (generated by makedist);
2000-09-13 wenzelm 2000-09-13 begin_theory: priority message to gain some robustness in sync communication;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-13 wenzelm 2000-09-13 LFilter: setmp quick_and_dirty false;
2000-09-13 wenzelm 2000-09-13 \<epsilon>: syntax (input);
2000-09-13 wenzelm 2000-09-13 tuned recdef hints;
2000-09-13 wenzelm 2000-09-13 easy settings: add /usr/local prefix; tuned;
2000-09-13 wenzelm 2000-09-13 updated to 3.3d;
2000-09-13 wenzelm 2000-09-13 tar packages: /usr/local;
2000-09-13 paulson 2000-09-13 more integer theorems, better simplification
2000-09-13 paulson 2000-09-13 moved Primes, Fib, Factorization from HOL/ex
2000-09-13 paulson 2000-09-13 zgcd now works for negative integers
2000-09-13 paulson 2000-09-13 moved Primes, Fib, Factorization to HOL/NumberTheory
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12 nipkow 2000-09-12 *** empty log message ***
2000-09-12 wenzelm 2000-09-12 tuned handling of "intros";
2000-09-12 wenzelm 2000-09-12 delrule: handle dest rules as well; replaced "delrule" by "rule del";
2000-09-12 wenzelm 2000-09-12 replaced "delrule" by "rule del";
2000-09-12 wenzelm 2000-09-12 renamed "delrule" to "rule del";
2000-09-12 wenzelm 2000-09-12 tuned;
2000-09-12 wenzelm 2000-09-12 tuned;
2000-09-12 nipkow 2000-09-12 *** empty log message ***
2000-09-12 nipkow 2000-09-12 *** empty log message ***
2000-09-12 wenzelm 2000-09-12 added MicroJava/document/root.bib;
2000-09-12 paulson 2000-09-12 tidying and updating for revised Mutilated Chess Board article
2000-09-11 wenzelm 2000-09-11 simple RPM spec for in-situ package;
2000-09-11 wenzelm 2000-09-11 template;
2000-09-11 wenzelm 2000-09-11 tuned;
2000-09-11 wenzelm 2000-09-11 simple RPM spec for in-situ package;
2000-09-11 wenzelm 2000-09-11 tuned;
2000-09-11 wenzelm 2000-09-11 updated;
2000-09-11 wenzelm 2000-09-11 renamed "rulify" to "rulified"; renamed "less_induct" to "nat_less_induct";
2000-09-11 wenzelm 2000-09-11 dummy;
2000-09-11 wenzelm 2000-09-11 updated;
2000-09-11 wenzelm 2000-09-11 improved WWW page generation (still somewhat experimental);
2000-09-11 wenzelm 2000-09-11 added title, abstract, bibliography;
2000-09-11 wenzelm 2000-09-11 proper markup of schematic (!) skolems;
2000-09-11 wenzelm 2000-09-11 support \isabellecontext;
2000-09-11 wenzelm 2000-09-11 define \isabellecontext;
2000-09-11 wenzelm 2000-09-11 added THIS;
2000-09-11 wenzelm 2000-09-11 case args: align_right;
2000-09-11 wenzelm 2000-09-11 added \isabellecontext; tuned;
2000-09-11 paulson 2000-09-11 tidied
2000-09-08 wenzelm 2000-09-08 *** empty log message ***
2000-09-07 wenzelm 2000-09-07 internalize error "insufficient syntax for prefix application";
2000-09-07 wenzelm 2000-09-07 tuned ML code (the_context, bind_thms(s));
2000-09-07 wenzelm 2000-09-07 HOL: qed_spec_mp now also removes bounded ALL; Isar: renamed some attributes;
2000-09-07 wenzelm 2000-09-07 tuned ML code (the_context, bind_thms(s));
2000-09-07 wenzelm 2000-09-07 updated attribute names;
2000-09-07 wenzelm 2000-09-07 improved att names;
2000-09-07 wenzelm 2000-09-07 use Rulify.rulify_no_asm;
2000-09-07 wenzelm 2000-09-07 print rule: priority;
2000-09-07 wenzelm 2000-09-07 improved att names / msgs;
2000-09-07 wenzelm 2000-09-07 avoid handle_error (better msgs);
2000-09-07 wenzelm 2000-09-07 tuned msgs;
2000-09-07 wenzelm 2000-09-07 tuned att names / msgs;