| Tue, 18 Oct 2005 17:59:29 +0200 | wenzelm | functor: no Simplifier argument; | changeset | files |
| Tue, 18 Oct 2005 17:59:28 +0200 | wenzelm | moved helper lemma to HilbertChoice.thy; | changeset | files |
| Tue, 18 Oct 2005 17:59:27 +0200 | wenzelm | Simplifier.theory_context; | changeset | files |
| Tue, 18 Oct 2005 17:59:26 +0200 | wenzelm | added lemma exE_some (from specification_package.ML); | changeset | files |
| Tue, 18 Oct 2005 17:59:25 +0200 | wenzelm | Simplifier.theory_context; | changeset | files |
| Tue, 18 Oct 2005 17:59:24 +0200 | wenzelm | tuned error msg; | changeset | files |
| Tue, 18 Oct 2005 17:59:23 +0200 | wenzelm | Simplifier.context/theory_context; | changeset | files |
| Tue, 18 Oct 2005 17:59:22 +0200 | wenzelm | updated; | changeset | files |