diff options
Diffstat (limited to '')
| -rw-r--r-- | spartan/data/More_Types.thy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/spartan/data/More_Types.thy b/spartan/data/More_Types.thy index fecf378..625f639 100644 --- a/spartan/data/More_Types.thy +++ b/spartan/data/More_Types.thy @@ -48,6 +48,9 @@ lemmas [elims ?s] = SumE and [comps] = Sum_comp_inl Sum_comp_inr +method left = rule Sum_inl +method right = rule Sum_inr + section \<open>Empty and unit types\<close> |