| Fri, 10 Feb 2006 02:22:39 +0100 | wenzelm | Local syntax depending on theory syntax. | changeset | files |
| Fri, 10 Feb 2006 02:22:37 +0100 | wenzelm | decode: observe Syntax.constN; | changeset | files |
| Fri, 10 Feb 2006 02:22:35 +0100 | wenzelm | removed obsolete add_typ/term_classes/tycons; | changeset | files |
| Fri, 10 Feb 2006 02:22:32 +0100 | wenzelm | tuned extern_term, pretty_term'; | changeset | files |
| Fri, 10 Feb 2006 02:22:29 +0100 | wenzelm | removed set quick_and_dirty and ThmDeps.enable -- no effect here; | changeset | files |
| Fri, 10 Feb 2006 02:22:24 +0100 | wenzelm | abbrevs: store in reverted orientation; | changeset | files |
| Fri, 10 Feb 2006 02:22:23 +0100 | wenzelm | use proof_general.ML: setmp quick_and_dirty captures default value; | changeset | files |