| Wed, 26 Jul 2006 13:31:07 +0200 | haftmann | added eval_term | changeset | files |
| Wed, 26 Jul 2006 11:32:55 +0200 | wenzelm | updated; | changeset | files |
| Wed, 26 Jul 2006 11:32:50 +0200 | wenzelm | fixed LaTeX problem; | changeset | files |
| Wed, 26 Jul 2006 10:09:25 +0200 | haftmann | added eval_term | changeset | files |
| Wed, 26 Jul 2006 09:50:23 +0200 | nipkow | Removed wrong sentence (Simon Funke) | changeset | files |
| Wed, 26 Jul 2006 00:44:49 +0200 | wenzelm | moved pprint functions to Isar/proof_display.ML; | changeset | files |
| Wed, 26 Jul 2006 00:44:48 +0200 | wenzelm | Tactical operations depending on local subgoal structure. | changeset | files |
| Wed, 26 Jul 2006 00:44:47 +0200 | wenzelm | moved pprint functions to Isar/proof_display.ML; | changeset | files |
| Wed, 26 Jul 2006 00:44:46 +0200 | wenzelm | export goal_tac (was internal refine_tac); | changeset | files |
| Wed, 26 Jul 2006 00:44:44 +0200 | wenzelm | added Pure/subgoal.ML; | changeset | files |
| Tue, 25 Jul 2006 23:17:42 +0200 | wenzelm | updated; | changeset | files |
| Tue, 25 Jul 2006 23:17:41 +0200 | wenzelm | raw symbols: disallow dot to avoid confusion in NameSpace.unpack; | changeset | files |
| Tue, 25 Jul 2006 21:18:12 +0200 | wenzelm | avoid Term.is_funtype; | changeset | files |
| Tue, 25 Jul 2006 21:18:11 +0200 | wenzelm | avoid structure Char; | changeset | files |
| Tue, 25 Jul 2006 21:18:09 +0200 | wenzelm | added variant_abs (from term.ML); | changeset | files |
| Tue, 25 Jul 2006 21:18:08 +0200 | wenzelm | added find_free (from term.ML); | changeset | files |