| Mon, 17 Oct 2005 23:10:24 +0200 | wenzelm | added type_solver (uses Simplifier.the_context); | changeset | files |
| Mon, 17 Oct 2005 23:10:23 +0200 | wenzelm | added pos/negDivAlg_induct declarations (from Main.thy); | changeset | files |
| Mon, 17 Oct 2005 23:10:22 +0200 | wenzelm | moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy; | changeset | files |
| Mon, 17 Oct 2005 23:10:21 +0200 | wenzelm | removed obsolete/experimental context components (superceded by Simplifier.the_context); | changeset | files |
| Mon, 17 Oct 2005 23:10:20 +0200 | wenzelm | added set/addloop' for simpset dependent loopers; | changeset | files |
| Mon, 17 Oct 2005 23:10:19 +0200 | wenzelm | functor: no Simplifier argument; | changeset | files |
| Mon, 17 Oct 2005 23:10:18 +0200 | wenzelm | change_claset(_of): more abtract interface; | changeset | files |