From 07c51b1801bd701bef61cedd571a944d9bd37e8b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 8 Jul 2020 15:55:48 +0200
Subject: 1. Initial `Definition` keyword. 2. ifelse.

---
 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 1efbb95..6729812 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -17,7 +17,7 @@ lemma
   Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A"
   unfolding Maybe_def none_def some_def by typechk+
 
-Lemma (derive) MaybeInd:
+Definition MaybeInd:
   assumes
     "A: U i"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
-- 
cgit v1.2.3