From 1ccd93665a01acdc25b37409e94b71615ced5393 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 May 2020 14:08:26 +0200
Subject: more List and Maybe

---
 spartan/data/Maybe.thy | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'spartan/data/Maybe.thy')

diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
index 98f5283..1efbb95 100644
--- a/spartan/data/Maybe.thy
+++ b/spartan/data/Maybe.thy
@@ -55,8 +55,10 @@ Lemma Maybe_comp_some:
 
 lemmas
   [intros] = MaybeF Maybe_none Maybe_some and
-  MaybeE [elims "?m"] = MaybeInd and
-  [comps] = Maybe_comp_none Maybe_comp_some
+  [comps] = Maybe_comp_none Maybe_comp_some and
+  MaybeE [elims "?m"] = MaybeInd[rotated 4]
+lemmas
+  Maybe_cases [cases] = MaybeE
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
-- 
cgit v1.2.3