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;
2000-09-07 wenzelm 2000-09-07 tuned;
2000-09-07 wenzelm 2000-09-07 linorder_cases;
2000-09-07 wenzelm 2000-09-07 chop_nonempty: accomodate new qed_spec_mp;
2000-09-07 wenzelm 2000-09-07 added linorder_cases; added Rulify.setup;
2000-09-07 wenzelm 2000-09-07 eliminated rulify setup (now in Provers/rulify.ML);
2000-09-07 wenzelm 2000-09-07 tuned msg;
2000-09-07 wenzelm 2000-09-07 updated rulify setup;
2000-09-07 wenzelm 2000-09-07 added Provers/rulify;
2000-09-07 wenzelm 2000-09-07 removed rulify_attrib_setup;
2000-09-07 wenzelm 2000-09-07 rulify setup;
2000-09-07 wenzelm 2000-09-07 added Provers/rulify.ML;
2000-09-07 wenzelm 2000-09-07 eliminated rulify stuff (now in Provers/rulify.ML);
2000-09-07 wenzelm 2000-09-07 updated setup;
2000-09-07 wenzelm 2000-09-07 setup Rulify.setup;
2000-09-07 wenzelm 2000-09-07 Conversion of object-level -->/ALL into meta-level ==>/!!;
2000-09-07 paulson 2000-09-07 a number of new theorems
2000-09-07 nipkow 2000-09-07 Added meaningful output to cong-error msg.
2000-09-07 paulson 2000-09-07 strengthened dvd_mod & proofed dvd_mod_iff
2000-09-06 wenzelm 2000-09-06 tuned;
2000-09-06 wenzelm 2000-09-06 make SML/NJ happy;
2000-09-06 wenzelm 2000-09-06 fixed structure U;
2000-09-06 nipkow 2000-09-06 less_induct -> nat_less_induct
2000-09-06 wenzelm 2000-09-06 tuned;
2000-09-06 nipkow 2000-09-06 imp_cong bound at thm level.
2000-09-06 paulson 2000-09-06 bug fix for arithmetic simprocs (nat & int)
2000-09-06 paulson 2000-09-06 tidied
2000-09-06 paulson 2000-09-06 new Iff theorem zero_le_succ_iff
2000-09-06 nipkow 2000-09-06 *** empty log message ***
2000-09-06 nipkow 2000-09-06 less_induct -> nat_less_induct
2000-09-05 wenzelm 2000-09-05 improved meson setup;
2000-09-05 wenzelm 2000-09-05 fixed quotes;
2000-09-05 wenzelm 2000-09-05 tuned;
2000-09-05 wenzelm 2000-09-05 proper handling of hints; tuned;
2000-09-05 wenzelm 2000-09-05 eliminated;
2000-09-05 wenzelm 2000-09-05 generalized types of args;
2000-09-05 wenzelm 2000-09-05 tuned output of isabelle env;
2000-09-05 wenzelm 2000-09-05 improved add_rules;
2000-09-05 wenzelm 2000-09-05 removed 'other' modifier;
2000-09-05 wenzelm 2000-09-05 added 'iff' declarations;
2000-09-05 wenzelm 2000-09-05 recdef hints (attributes and modifiers);
2000-09-05 wenzelm 2000-09-05 use 'iff' modifier;
2000-09-05 wenzelm 2000-09-05 RecdefPackage.add_recdef_old;