1999-04-16 wenzelm 1999-04-16 added Isar_examples;
1999-04-16 wenzelm 1999-04-16 Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
1999-04-16 wenzelm 1999-04-16 lemmas about proper subset relation;
1999-04-16 wenzelm 1999-04-16 Proof by induction on types / set / functions.
1999-04-16 wenzelm 1999-04-16 print_datatypes;
1999-04-16 wenzelm 1999-04-16 added Tools/induct_method.ML;
1999-04-16 wenzelm 1999-04-16 'HOL/recdef' theory data;
1999-04-16 wenzelm 1999-04-16 'HOL/recdef' theory data; induct method setup;
1999-04-16 wenzelm 1999-04-16 'HOL/inductive' theory data;
1999-04-16 wenzelm 1999-04-16 Sign.base_name fid;
1999-04-16 wenzelm 1999-04-16 added incr_indexes, incr_indexes_wrt;
1999-04-15 nipkow 1999-04-15 Proof mod.
1999-04-15 nipkow 1999-04-15 Added new thms.
1999-04-14 wenzelm 1999-04-14 quiet_mode;
1999-04-14 wenzelm 1999-04-14 Tools/inductive_package.ML;
1999-04-14 wenzelm 1999-04-14 triple_swap;
1999-04-14 wenzelm 1999-04-14 Wrapper module for Konrad Slind's TFL package.
1999-04-14 wenzelm 1999-04-14 remoced old set_current_thy;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 intrs: names and atts;
1999-04-14 wenzelm 1999-04-14 tuned comments; tuned types;
1999-04-14 wenzelm 1999-04-14 tuned comments; intrs: names and atts; Isar outer syntax;
1999-04-14 wenzelm 1999-04-14 tuned comments;
1999-04-14 wenzelm 1999-04-14 intrs: provide names and atts;
1999-04-14 wenzelm 1999-04-14 cleaned comments;
1999-04-14 wenzelm 1999-04-14 tuned;
1999-04-14 wenzelm 1999-04-14 fixed named type infixes (actual BUG!);
1999-04-13 wenzelm 1999-04-13 updated isatool install;
1999-04-13 wenzelm 1999-04-13 -p option; -k option;
1999-04-13 wenzelm 1999-04-13 adapted isatool install;
1999-04-13 wenzelm 1999-04-13 improved isatool install;
1999-04-13 wenzelm 1999-04-13 tuned;
1999-04-12 wenzelm 1999-04-12 ML_PLATFORM;
1999-04-12 wenzelm 1999-04-12 ML_PLATFORM;
1999-04-07 wenzelm 1999-04-07 fixed @@;
1999-04-04 paulson 1999-04-04 fixed bib file
1999-04-03 wenzelm 1999-04-03 fixed;
1999-04-01 pusch 1999-04-01 new definition for nth. added warnings, if primrec definition is deleted from simpset.
1999-03-31 nipkow 1999-03-31 useless relic
1999-03-30 nipkow 1999-03-30 arith_tac
1999-03-19 wenzelm 1999-03-19 tuned;
1999-03-19 wenzelm 1999-03-19 common qed and end of proofs;
1999-03-18 nipkow 1999-03-18 * New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
1999-03-18 nipkow 1999-03-18 New bounded quantifier syntax: !x<i. P etc
1999-03-18 paulson 1999-03-18 added new theory Yahalom_Bad
1999-03-18 paulson 1999-03-18 added new theory Yahalom_Bad
1999-03-18 paulson 1999-03-18 exchanged the order of Gets and Notes in datatype event
1999-03-17 wenzelm 1999-03-17 fixed thm_name again;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 xnum token class;
1999-03-17 wenzelm 1999-03-17 xstr token class;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 fixed axclass_tac;
1999-03-17 wenzelm 1999-03-17 tuned;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1999-03-17 wenzelm 1999-03-17 fixed msg;
1999-03-17 wenzelm 1999-03-17 tuned msg;
1999-03-17 wenzelm 1999-03-17 axclass_tac lost an argument;
1999-03-17 wenzelm 1999-03-17 HOL/typedef: fixed type inference for representing set; AxClass.axclass_tac lost the theory argument;