diff options
| author | Josh Chen | 2020-05-24 20:44:33 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-24 20:44:33 +0200 |
| commit | 3ad2f03f7dbc922e2c711241146db091d193003d (patch) | |
| tree | 6db26730510b119bf10dc836d21a9869ace6c416 /spartan/theories/Identity.thy | |
| parent | 6f37e6b72905eff8f2c7078823e5577bc5b55eb0 (diff) | |
new work on elimination tactic
Diffstat (limited to '')
| -rw-r--r-- | spartan/theories/Identity.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 4a4cc40..3f16f4c 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -40,7 +40,7 @@ axiomatization where lemmas [intros] = IdF IdI and - [elims] = IdE and + [elims "?p" (*"?x" "?y"*)] = IdE and [comps] = Id_comp |