| Fri, 19 Jul 2013 15:48:04 +0200 | nipkow | added exerciese | changeset | files |
| Fri, 19 Jul 2013 12:00:31 +0200 | traytel | do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms) | changeset | files |
| Thu, 18 Jul 2013 23:13:44 +0200 | wenzelm | modify background theory where it is actually required (cf. 51dfdcd88e84); | changeset | files |
| Thu, 18 Jul 2013 22:32:00 +0200 | wenzelm | tuned messages -- avoid text folds stemming from Pretty.chunks; | changeset | files |
| Thu, 18 Jul 2013 22:18:20 +0200 | wenzelm | proper system options for 'find_theorems'; | changeset | files |
| Thu, 18 Jul 2013 22:00:35 +0200 | wenzelm | guard unify tracing via visible status of global theory; | changeset | files |