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;
1999-03-17 wenzelm 1999-03-17 rep_datatype: '_i' version, attributes, outer syntax;
1999-03-17 wenzelm 1999-03-17 local open OuterParse;
1999-03-17 wenzelm 1999-03-17 actually check non-emptiness theorem; added typedef_proof(_i); 'typedef' outer syntax;
1999-03-17 wenzelm 1999-03-17 fixed typedef representing set;
1999-03-17 wenzelm 1999-03-17 adapted rep_datatype;
1999-03-17 wenzelm 1999-03-17 added dest_mem;
1999-03-17 wenzelm 1999-03-17 theory data; attributes for class axioms; instance_subclass/arity_proof(_i); expand_classes proof method; 'axclass' / 'instance' outer syntax;
1999-03-17 wenzelm 1999-03-17 adapted AxClass.add_axclass; PureThy.get_thm axioms;
1999-03-17 wenzelm 1999-03-17 tuned msgs; removed verbose flag;
1999-03-17 wenzelm 1999-03-17 tuned;
1999-03-17 wenzelm 1999-03-17 cleaned comments;
1999-03-17 wenzelm 1999-03-17 added apply_cond_open;
1999-03-17 wenzelm 1999-03-17 added (improper_)command;
1999-03-17 wenzelm 1999-03-17 added simple_arity, spec_name, spec_opt_name; tuned thm_name; xthms1: no 'and' separators;