diff options
Diffstat (limited to 'spartan/theories/Identity.thy')
| -rw-r--r-- | spartan/theories/Identity.thy | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 01bea46..3a982f6 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -41,7 +41,8 @@ axiomatization where lemmas [intros] = IdF IdI and [elims "?p" "?a" "?b"] = IdE and - [comps] = Id_comp + [comps] = Id_comp and + [refl] = IdI section \<open>Path induction\<close> |