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/Spartan.thy | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'spartan/core/Spartan.thy')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 0a5fe4c..ed21934 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -6,7 +6,7 @@ imports
   "HOL-Eisbach.Eisbach"
   "HOL-Eisbach.Eisbach_Tools"
 keywords
-  "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
+  "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
   "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
   "congruence" "print_coercions" :: thy_decl and
   "rhs" "derive" "prems" "vars" :: quasi_command
@@ -150,28 +150,29 @@ axiomatization where
     \<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
 
 
-section \<open>Proof commands\<close>
+section \<open>Infrastructure\<close>
+
+ML_file \<open>lib.ML\<close>
+ML_file \<open>types.ML\<close>
+
+subsection \<open>Proof commands\<close>
 
 named_theorems typechk
 
-ML_file \<open>lib.ML\<close>
 ML_file \<open>goals.ML\<close>
 ML_file \<open>focus.ML\<close>
-ML_file \<open>types.ML\<close>
 
-
-section \<open>Congruence automation\<close>
+subsection \<open>Congruence automation\<close>
 
 consts "rhs" :: \<open>'a\<close> ("..")
 
 ML_file \<open>congruence.ML\<close>
 
-
-section \<open>Methods\<close>
-
 ML_file \<open>elimination.ML\<close> \<comment> \<open>elimination rules\<close>
 ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close>
 
+subsection \<open>Methods\<close>
+
 named_theorems intros and comps
 lemmas
   [intros] = PiF PiI SigF SigI and
@@ -275,8 +276,7 @@ setup \<open>map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" typechk
 
 method reduce uses add = (simp add: comps add | subst comps)+
 
-
-section \<open>Implicit notations\<close>
+subsection \<open>Implicits\<close>
 
 text \<open>
   \<open>?\<close> is used to mark implicit arguments in definitions, while \<open>{}\<close> is expanded
@@ -301,8 +301,7 @@ text \<open>Automatically insert inhabitation judgments where needed:\<close>
 syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
 translations "inhabited A" \<rightharpoonup> "CONST has_type {} A"
 
-
-section \<open>Lambda coercion\<close>
+subsection \<open>Lambda coercion\<close>
 
 \<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
 abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
-- 
cgit v1.2.3