2002-01-17 nipkow 2002-01-17 Added code generation to Scanner.thy Renamed Union -> Or, union -> or
2002-01-17 kleing 2002-01-17 registered directly executable version with the code generator
2002-01-17 nipkow 2002-01-17 *** empty log message ***
2002-01-17 paulson 2002-01-17 new definitions from Sidi Ehmety
2002-01-17 paulson 2002-01-17 made proofs more robust
2002-01-17 paulson 2002-01-17 mistakenly deleted this theory
2002-01-17 kleing 2002-01-17 fixed
2002-01-16 wenzelm 2002-01-16 GPLed;
2002-01-16 wenzelm 2002-01-16 added rewrite_term; tuned; GPLed;
2002-01-16 wenzelm 2002-01-16 interface to Pattern.rewrite_term;
2002-01-16 wenzelm 2002-01-16 tune norm_hhf_tac;
2002-01-16 wenzelm 2002-01-16 added beta_eta_contract;
2002-01-16 wenzelm 2002-01-16 tuned title;
2002-01-16 wenzelm 2002-01-16 export beta_eta_conversion;
2002-01-16 wenzelm 2002-01-16 Interface/proof_general.ML move to proof_general.ML;
2002-01-16 paulson 2002-01-16 Isar version of ZF/AC
2002-01-16 paulson 2002-01-16 Isar version of AC
2002-01-16 wenzelm 2002-01-16 norm_hhf;
2002-01-15 kleing 2002-01-15 fixed theory deps
2002-01-15 kleing 2002-01-15 use exec_lub instead of some_lub
2002-01-15 kleing 2002-01-15 tuned for directly executable definitions
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-15 wenzelm 2002-01-15 removed second copy of show_hyps;
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-15 wenzelm 2002-01-15 allow empty locales;
2002-01-15 wenzelm 2002-01-15 updated;
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-15 paulson 2002-01-15 new theorem
2002-01-15 paulson 2002-01-15 stylistic changes
2002-01-15 paulson 2002-01-15 now [rule_format] knows about ospec
2002-01-15 paulson 2002-01-15 split can now be unfolded even with one argument
2002-01-15 wenzelm 2002-01-15 save: be slightly more about absent tags; get/add: missing case_names default to numbers 1, 2, 3, ...;
2002-01-15 wenzelm 2002-01-15 allow zero goals;
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-15 wenzelm 2002-01-15 print_locale: allow full body specification;
2002-01-15 wenzelm 2002-01-15 added mk_conjunction_list;
2002-01-15 wenzelm 2002-01-15 conj_intr_list and conj_elim_precise: cover 0 conjuncts;
2002-01-15 wenzelm 2002-01-15 removed case_numbers (already covered by default);
2002-01-15 wenzelm 2002-01-15 Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
2002-01-14 wenzelm 2002-01-14 * system: reduced base memory usage by Poly/ML (approx. 20 MB instead of 40 MB), cf. ML_OPTIONS;
2002-01-14 wenzelm 2002-01-14 ML_OPTIONS="-h 15000" (used to be 30000);
2002-01-14 wenzelm 2002-01-14 updated;
2002-01-14 wenzelm 2002-01-14 tuned;
2002-01-14 wenzelm 2002-01-14 updated;
2002-01-14 wenzelm 2002-01-14 tuned;
2002-01-14 wenzelm 2002-01-14 updated;
2002-01-14 wenzelm 2002-01-14 tuned;
2002-01-14 wenzelm 2002-01-14 updated;
2002-01-14 wenzelm 2002-01-14 tuned;
2002-01-14 wenzelm 2002-01-14 tuned;
2002-01-14 oheimb 2002-01-14 cosmetics
2002-01-13 wenzelm 2002-01-13 \<twosuperior> syntax moved to HOL/Numerals;
2002-01-13 wenzelm 2002-01-13 tuned;
2002-01-13 wenzelm 2002-01-13 prime_dvd_power_two;
2002-01-13 wenzelm 2002-01-13 symbolic syntax for x^2 (faills back on plain infix "^");
2002-01-13 wenzelm 2002-01-13 \usepackage[latin1]{inputenc};
2002-01-13 wenzelm 2002-01-13 * HOL: symbolic syntax for x^2 (numeral 2);
2002-01-13 wenzelm 2002-01-13 added HOL/Real/document/root.tex;
2002-01-13 wenzelm 2002-01-13 HOL-Real/Complex_Numbers;
2002-01-13 wenzelm 2002-01-13 Real/Complex_Numbers.thy;