Tue, 15 Jan 2002 22:22:05 +0100 |
kleing |
use exec_lub instead of some_lub
|
changeset |
files
|
Tue, 15 Jan 2002 22:21:30 +0100 |
kleing |
tuned for directly executable definitions
|
changeset |
files
|
Tue, 15 Jan 2002 21:09:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 15 Jan 2002 21:09:01 +0100 |
wenzelm |
removed second copy of show_hyps;
|
changeset |
files
|
Tue, 15 Jan 2002 18:51:20 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 15 Jan 2002 18:43:51 +0100 |
wenzelm |
allow empty locales;
|
changeset |
files
|
Tue, 15 Jan 2002 17:54:31 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Tue, 15 Jan 2002 17:54:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 15 Jan 2002 15:07:41 +0100 |
paulson |
new theorem
|
changeset |
files
|
Tue, 15 Jan 2002 13:14:39 +0100 |
paulson |
stylistic changes
|
changeset |
files
|
Tue, 15 Jan 2002 10:24:20 +0100 |
paulson |
now [rule_format] knows about ospec
|
changeset |
files
|
Tue, 15 Jan 2002 10:23:58 +0100 |
paulson |
split can now be unfolded even with one argument
|
changeset |
files
|
Tue, 15 Jan 2002 00:13:20 +0100 |
wenzelm |
save: be slightly more about absent tags;
|
changeset |
files
|
Tue, 15 Jan 2002 00:12:21 +0100 |
wenzelm |
allow zero goals;
|
changeset |
files
|
Tue, 15 Jan 2002 00:11:52 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 15 Jan 2002 00:11:30 +0100 |
wenzelm |
print_locale: allow full body specification;
|
changeset |
files
|
Tue, 15 Jan 2002 00:09:54 +0100 |
wenzelm |
added mk_conjunction_list;
|
changeset |
files
|
Tue, 15 Jan 2002 00:09:29 +0100 |
wenzelm |
conj_intr_list and conj_elim_precise: cover 0 conjuncts;
|
changeset |
files
|
Tue, 15 Jan 2002 00:08:51 +0100 |
wenzelm |
removed case_numbers (already covered by default);
|
changeset |
files
|
Tue, 15 Jan 2002 00:08:11 +0100 |
wenzelm |
Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
|
changeset |
files
|
Mon, 14 Jan 2002 17:45:30 +0100 |
wenzelm |
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead
|
changeset |
files
|
Mon, 14 Jan 2002 17:43:44 +0100 |
wenzelm |
ML_OPTIONS="-h 15000" (used to be 30000);
|
changeset |
files
|
Mon, 14 Jan 2002 17:31:45 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 14 Jan 2002 17:31:42 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 14 Jan 2002 17:29:25 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 14 Jan 2002 17:29:12 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 14 Jan 2002 17:23:40 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 14 Jan 2002 17:23:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 14 Jan 2002 16:09:29 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Mon, 14 Jan 2002 16:09:25 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 14 Jan 2002 14:39:22 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 14 Jan 2002 00:16:43 +0100 |
oheimb |
cosmetics
|
changeset |
files
|
Sun, 13 Jan 2002 21:14:51 +0100 |
wenzelm |
\<twosuperior> syntax moved to HOL/Numerals;
|
changeset |
files
|
Sun, 13 Jan 2002 21:14:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 13 Jan 2002 21:14:14 +0100 |
wenzelm |
prime_dvd_power_two;
|
changeset |
files
|
Sun, 13 Jan 2002 21:13:59 +0100 |
wenzelm |
symbolic syntax for x^2 (faills back on plain infix "^");
|
changeset |
files
|
Sun, 13 Jan 2002 21:13:27 +0100 |
wenzelm |
\usepackage[latin1]{inputenc};
|
changeset |
files
|
Sun, 13 Jan 2002 21:12:43 +0100 |
wenzelm |
* HOL: symbolic syntax for x^2 (numeral 2);
|
changeset |
files
|
Sun, 13 Jan 2002 21:09:17 +0100 |
wenzelm |
added HOL/Real/document/root.tex;
|
changeset |
files
|
Sun, 13 Jan 2002 19:45:17 +0100 |
wenzelm |
HOL-Real/Complex_Numbers;
|
changeset |
files
|
Sun, 13 Jan 2002 19:42:30 +0100 |
wenzelm |
Real/Complex_Numbers.thy;
|
changeset |
files
|
Sat, 12 Jan 2002 22:44:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 12 Jan 2002 22:24:09 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 12 Jan 2002 22:17:08 +0100 |
wenzelm |
produce predicate text;
|
changeset |
files
|
Sat, 12 Jan 2002 22:15:48 +0100 |
wenzelm |
added atomize_cterm;
|
changeset |
files
|
Sat, 12 Jan 2002 16:55:53 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 12 Jan 2002 16:40:02 +0100 |
wenzelm |
unify_frozen: proper use of maxidx';
|
changeset |
files
|
Sat, 12 Jan 2002 16:38:42 +0100 |
wenzelm |
paramify_dummies: proper treatment of maxidx;
|
changeset |
files
|
Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
changeset |
files
|
Fri, 11 Jan 2002 18:49:25 +0100 |
wenzelm |
Isabelle2002 (January 2002);
|
changeset |
files
|
Fri, 11 Jan 2002 18:07:45 +0100 |
wenzelm |
removed obsolete isamode.ML;
|
changeset |
files
|
Fri, 11 Jan 2002 18:07:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 11 Jan 2002 17:04:49 +0100 |
wenzelm |
#!/usr/bin/env bash;
|
changeset |
files
|
Fri, 11 Jan 2002 14:53:30 +0100 |
wenzelm |
replace gen_all by forall_elim_vars_safe;
|
changeset |
files
|
Fri, 11 Jan 2002 14:53:05 +0100 |
wenzelm |
improved forall_elim_vars_safe (no longer invents new indexes);
|
changeset |
files
|
Fri, 11 Jan 2002 14:44:58 +0100 |
wenzelm |
lemmas (in ACe) AC;
|
changeset |
files
|
Fri, 11 Jan 2002 14:44:24 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 11 Jan 2002 00:35:03 +0100 |
wenzelm |
IsarThy.theorems_i;
|
changeset |
files
|
Fri, 11 Jan 2002 00:34:43 +0100 |
wenzelm |
moved setmksimps to Main!
|
changeset |
files
|
Fri, 11 Jan 2002 00:33:35 +0100 |
wenzelm |
have_thmss vs. have_thmss_i;
|
changeset |
files
|