Thu, 17 Jan 2002 15:06:36 +0100 kleing registered directly executable version with the code generator
Thu, 17 Jan 2002 12:58:31 +0100 nipkow *** empty log message ***
Thu, 17 Jan 2002 12:45:52 +0100 paulson new definitions from Sidi Ehmety
Thu, 17 Jan 2002 12:45:36 +0100 paulson made proofs more robust
Thu, 17 Jan 2002 10:35:59 +0100 paulson mistakenly deleted this theory
Thu, 17 Jan 2002 09:01:10 +0100 kleing fixed
Wed, 16 Jan 2002 23:19:34 +0100 wenzelm GPLed;
Wed, 16 Jan 2002 23:18:20 +0100 wenzelm added rewrite_term;
Wed, 16 Jan 2002 23:17:44 +0100 wenzelm interface to Pattern.rewrite_term;
Wed, 16 Jan 2002 22:24:37 +0100 wenzelm tune norm_hhf_tac;
Wed, 16 Jan 2002 22:23:46 +0100 wenzelm added beta_eta_contract;
Wed, 16 Jan 2002 21:01:08 +0100 wenzelm tuned title;
Wed, 16 Jan 2002 20:58:27 +0100 wenzelm export beta_eta_conversion;
Wed, 16 Jan 2002 20:57:02 +0100 wenzelm Interface/proof_general.ML move to proof_general.ML;
Wed, 16 Jan 2002 17:53:22 +0100 paulson Isar version of ZF/AC
Wed, 16 Jan 2002 17:52:06 +0100 paulson Isar version of AC
Wed, 16 Jan 2002 15:04:37 +0100 wenzelm norm_hhf;
Tue, 15 Jan 2002 23:23:09 +0100 kleing fixed theory deps
Tue, 15 Jan 2002 22:22:05 +0100 kleing use exec_lub instead of some_lub
Tue, 15 Jan 2002 22:21:30 +0100 kleing tuned for directly executable definitions
Tue, 15 Jan 2002 21:09:31 +0100 wenzelm tuned;
Tue, 15 Jan 2002 21:09:01 +0100 wenzelm removed second copy of show_hyps;
Tue, 15 Jan 2002 18:51:20 +0100 wenzelm tuned;
Tue, 15 Jan 2002 18:43:51 +0100 wenzelm allow empty locales;
Tue, 15 Jan 2002 17:54:31 +0100 wenzelm updated;
Tue, 15 Jan 2002 17:54:28 +0100 wenzelm tuned;
Tue, 15 Jan 2002 15:07:41 +0100 paulson new theorem
Tue, 15 Jan 2002 13:14:39 +0100 paulson stylistic changes
Tue, 15 Jan 2002 10:24:20 +0100 paulson now [rule_format] knows about ospec
Tue, 15 Jan 2002 10:23:58 +0100 paulson split can now be unfolded even with one argument
Tue, 15 Jan 2002 00:13:20 +0100 wenzelm save: be slightly more about absent tags;
Tue, 15 Jan 2002 00:12:21 +0100 wenzelm allow zero goals;
Tue, 15 Jan 2002 00:11:52 +0100 wenzelm tuned;
Tue, 15 Jan 2002 00:11:30 +0100 wenzelm print_locale: allow full body specification;
Tue, 15 Jan 2002 00:09:54 +0100 wenzelm added mk_conjunction_list;
Tue, 15 Jan 2002 00:09:29 +0100 wenzelm conj_intr_list and conj_elim_precise: cover 0 conjuncts;
Tue, 15 Jan 2002 00:08:51 +0100 wenzelm removed case_numbers (already covered by default);
Tue, 15 Jan 2002 00:08:11 +0100 wenzelm Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
Mon, 14 Jan 2002 17:45:30 +0100 wenzelm * system: reduced base memory usage by Poly/ML (approx. 20 MB instead
Mon, 14 Jan 2002 17:43:44 +0100 wenzelm ML_OPTIONS="-h 15000" (used to be 30000);
Mon, 14 Jan 2002 17:31:45 +0100 wenzelm updated;
Mon, 14 Jan 2002 17:31:42 +0100 wenzelm tuned;
Mon, 14 Jan 2002 17:29:25 +0100 wenzelm updated;
Mon, 14 Jan 2002 17:29:12 +0100 wenzelm tuned;
Mon, 14 Jan 2002 17:23:40 +0100 wenzelm updated;
Mon, 14 Jan 2002 17:23:35 +0100 wenzelm tuned;
Mon, 14 Jan 2002 16:09:29 +0100 wenzelm updated;
Mon, 14 Jan 2002 16:09:25 +0100 wenzelm tuned;
Mon, 14 Jan 2002 14:39:22 +0100 wenzelm tuned;
Mon, 14 Jan 2002 00:16:43 +0100 oheimb cosmetics
Sun, 13 Jan 2002 21:14:51 +0100 wenzelm \<twosuperior> syntax moved to HOL/Numerals;
Sun, 13 Jan 2002 21:14:31 +0100 wenzelm tuned;
Sun, 13 Jan 2002 21:14:14 +0100 wenzelm prime_dvd_power_two;
Sun, 13 Jan 2002 21:13:59 +0100 wenzelm symbolic syntax for x^2 (faills back on plain infix "^");
Sun, 13 Jan 2002 21:13:27 +0100 wenzelm \usepackage[latin1]{inputenc};
Sun, 13 Jan 2002 21:12:43 +0100 wenzelm * HOL: symbolic syntax for x^2 (numeral 2);
Sun, 13 Jan 2002 21:09:17 +0100 wenzelm added HOL/Real/document/root.tex;
Sun, 13 Jan 2002 19:45:17 +0100 wenzelm HOL-Real/Complex_Numbers;
Sun, 13 Jan 2002 19:42:30 +0100 wenzelm Real/Complex_Numbers.thy;
Sat, 12 Jan 2002 22:44:10 +0100 wenzelm tuned;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip