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/core/goals.ML | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'spartan/core/goals.ML')

diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 9f394f0..4b53a7f 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -204,11 +204,20 @@ fun theorem spec descr =
         schematic_theorem_cmd
           (case opt_derive of SOME "derive" => true | _ => false)
           long descr NONE (K I) binding includes elems concl))
+
+fun definition spec descr =
+  Outer_Syntax.local_theory_to_proof' spec "definition via proof"
+    ((long_statement || short_statement) >>
+      (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd
+        true long descr NONE (K I) binding includes elems concl))
+
+
 in
 
 val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem"
 val _ = theorem \<^command_keyword>\<open>Lemma\<close> "Lemma"
 val _ = theorem \<^command_keyword>\<open>Corollary\<close> "Corollary"
 val _ = theorem \<^command_keyword>\<open>Proposition\<close> "Proposition"
+val _ = definition \<^command_keyword>\<open>Definition\<close> "Definition"
 
 end
-- 
cgit v1.2.3