| Tue, 21 Mar 2006 12:16:43 +0100 |
paulson |
Removal of unnecessary simprules: simproc cancel_numerals now works without
|
changeset |
files
|
| Mon, 20 Mar 2006 21:29:04 +0100 |
wenzelm |
interpret: Proof.assert_forward_or_chain;
|
changeset |
files
|
| Mon, 20 Mar 2006 17:38:22 +0100 |
paulson |
subsetI is often necessary
|
changeset |
files
|
| Mon, 20 Mar 2006 17:37:11 +0100 |
paulson |
Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer
|
changeset |
files
|
| Mon, 20 Mar 2006 17:15:35 +0100 |
ballarin |
Tuned signature of Locale.add_locale(_i).
|
changeset |
files
|
| Sat, 18 Mar 2006 20:10:51 +0100 |
wenzelm |
simplified mg_domain (use Sign.classes/arities_of);
|
changeset |
files
|
| Sat, 18 Mar 2006 20:10:50 +0100 |
wenzelm |
made $$ and "this" monomorphic (string);
|
changeset |
files
|
| Sat, 18 Mar 2006 20:10:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 18 Mar 2006 20:10:48 +0100 |
wenzelm |
export arities_of instead of classes_arities_of;
|
changeset |
files
|
| Sat, 18 Mar 2006 18:33:49 +0100 |
wenzelm |
updated;
|
changeset |
files
|
| Sat, 18 Mar 2006 18:33:40 +0100 |
wenzelm |
renamed const less to lt;
|
changeset |
files
|
| Sat, 18 Mar 2006 09:58:49 +0100 |
haftmann |
renamed constant less in lattice
|
changeset |
files
|
| Fri, 17 Mar 2006 22:33:06 +0100 |
nipkow |
fixed problem with proof reconstruction by adding add_Suc to arith-simpset.
|
changeset |
files
|
| Fri, 17 Mar 2006 17:38:38 +0100 |
schirmer |
added parser locale_expr_unless
|
changeset |
files
|
| Fri, 17 Mar 2006 16:17:38 +0100 |
haftmann |
fixed clsvar bug
|
changeset |
files
|