| Mon, 16 Jun 2008 22:13:47 +0200 | wenzelm | removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML); | changeset | files |
| Mon, 16 Jun 2008 22:13:46 +0200 | wenzelm | inst1_tac: proper context; | changeset | files |
| Mon, 16 Jun 2008 22:13:39 +0200 | wenzelm | pervasive RuleInsts; | changeset | files |
| Mon, 16 Jun 2008 17:56:08 +0200 | wenzelm | updated generated file; | changeset | files |
| Mon, 16 Jun 2008 17:54:51 +0200 | wenzelm | converted ML proofs; | changeset | files |
| Mon, 16 Jun 2008 17:54:50 +0200 | wenzelm | added read_instantiate; | changeset | files |
| Mon, 16 Jun 2008 17:54:49 +0200 | wenzelm | ML tactic: do not abstract over context again; | changeset | files |