| Wed, 22 Mar 2006 11:14:58 +0100 | nipkow | translations -> abbreviations (a cool feature) | changeset | files |
| Tue, 21 Mar 2006 15:38:53 +0100 | wenzelm | fixed example; | changeset | files |
| Tue, 21 Mar 2006 12:18:22 +0100 | wenzelm | mark_boundT: produce well-typed term; | changeset | files |
| Tue, 21 Mar 2006 12:18:21 +0100 | wenzelm | subtract (op =); | changeset | files |
| Tue, 21 Mar 2006 12:18:20 +0100 | wenzelm | avoid polymorphic equality; | changeset | files |
| Tue, 21 Mar 2006 12:18:19 +0100 | wenzelm | avoid polymorphic equality; | changeset | files |
| Tue, 21 Mar 2006 12:18:18 +0100 | wenzelm | moved gen_eq_set to library.ML; | changeset | files |
| Tue, 21 Mar 2006 12:18:17 +0100 | wenzelm | added ~$$ (negative literal); | changeset | files |
| Tue, 21 Mar 2006 12:18:15 +0100 | wenzelm | avoid polymorphic equality; | changeset | files |
| Tue, 21 Mar 2006 12:18:13 +0100 | wenzelm | remove (op =); | changeset | files |
| Tue, 21 Mar 2006 12:18:11 +0100 | wenzelm | gen_eq_set, remove (op =); | changeset | files |
| Tue, 21 Mar 2006 12:18:10 +0100 | wenzelm | abbreviation upto, length; | changeset | files |
| Tue, 21 Mar 2006 12:18:09 +0100 | wenzelm | added subtract; | changeset | files |
| Tue, 21 Mar 2006 12:18:07 +0100 | wenzelm | subtract (op =); | changeset | files |
| Tue, 21 Mar 2006 12:18:06 +0100 | wenzelm | remove (op =); | changeset | files |
| Tue, 21 Mar 2006 12:17:38 +0100 | paulson | Now SML/NJ-friendly (IntInf) | changeset | files |
| 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 |