| Sat, 16 Apr 2011 20:49:48 +0200 | wenzelm | proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; | changeset | files |
| Sat, 16 Apr 2011 20:30:44 +0200 | wenzelm | more direct Thm.cprem_of (with exception THM instead of Subscript); | changeset | files |
| Sat, 16 Apr 2011 20:26:59 +0200 | wenzelm | more direct Thm.cprem_of (with exception THM instead of Subscript); | changeset | files |