diff options
| author | Josh Chen | 2020-07-21 16:28:05 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-21 16:28:05 +0200 |
| commit | 306721649f0963ab225deb8d5670cfe196bb360d (patch) | |
| tree | d44a93c55215bd24d9b9938418d6058d0343cf4e /spartan/core/cases.ML | |
| parent | dfd241b2d85fc5a4ad4d7ddd64adf0138b05f083 (diff) | |
1. Bugfix: implicits now properly name schematic variables. Fixes problems caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy.
Diffstat (limited to 'spartan/core/cases.ML')
0 files changed, 0 insertions, 0 deletions