From 77aa10763429d2ded040071fbf7bee331dd52f5e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 31 Jul 2020 18:10:10 +0200
Subject: (REF) Tweak attribute names in preparation for new logical
 introduction rule behavior

---
 spartan/lib/Maybe.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index a2e1638..0a7ec21 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -56,7 +56,7 @@ Lemma Maybe_comp_some:
 
 lemmas
   [form] = MaybeF and
-  [intro, intros] = Maybe_none Maybe_some and
+  [intr, intro] = Maybe_none Maybe_some and
   [comp] = Maybe_comp_none Maybe_comp_some and
   MaybeE [elim "?m"] = MaybeInd[rotated 4]
 lemmas
-- 
cgit v1.2.3