diff options
Diffstat (limited to '')
| -rw-r--r-- | spartan/data/More_Types.thy (renamed from hott/More_Types.thy) | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/hott/More_Types.thy b/spartan/data/More_Types.thy index d29d794..f0cee6d 100644 --- a/hott/More_Types.thy +++ b/spartan/data/More_Types.thy @@ -44,7 +44,7 @@ axiomatization where lemmas [intros] = SumF Sum_inl Sum_inr and - [elims] = SumE and + [elims ?s] = SumE and [comps] = Sum_comp_inl Sum_comp_inr @@ -75,7 +75,8 @@ and lemmas [intros] = TopF TopI BotF and - [elims] = TopE BotE and + [elims ?a] = TopE and + [elims ?x] = BotE and [comps] = Top_comp |