diff options
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Nat.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/Nat.thy b/hott/Nat.thy index 3d938cd..bd58fbc 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -39,7 +39,7 @@ where lemmas [intros] = NatF Nat_zero Nat_suc and - [elims] = NatE and + [elims "?n"] = NatE and [comps] = Nat_comp_zero Nat_comp_suc text \<open>Non-dependent recursion\<close> |