1 files changed, 25 insertions, 23 deletions
diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy
index 5888a90..29c7248 100644
--- a/mltt/core/MLTT.thy
+++ b/mltt/core/MLTT.thy
@@ -220,6 +220,27 @@ in
 end
 \<close>
 
+section \<open>Implicits\<close>
+
+text \<open>
+  \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
+  immediately for elaboration in statements.
+\<close>
+
+consts
+  iarg :: \<open>'a\<close> ("{}")
+  hole :: \<open>'b\<close> ("?")
+
+ML_file \<open>implicits.ML\<close>
+
+attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
+
+ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close>
+
+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>Statements and goals\<close>
 
@@ -228,6 +249,10 @@ ML_file \<open>elaboration.ML\<close>
 ML_file \<open>elaborated_statement.ML\<close>
 ML_file \<open>goals.ML\<close>
 
+text \<open>Syntax for definition bodies.\<close>
+syntax defn :: \<open>o \<Rightarrow> prop\<close> ("(:=_)")
+translations "defn t" \<rightharpoonup> "CONST has_type t ?"
+
 
 section \<open>Proof methods\<close>
 
@@ -328,29 +353,6 @@ consts "rhs" :: \<open>'a\<close> ("..")
 ML_file \<open>calc.ML\<close>
 
 
-section \<open>Implicits\<close>
-
-text \<open>
-  \<open>{}\<close> is used to mark implicit arguments in definitions, while \<open>?\<close> is expanded
-  immediately for elaboration in statements.
-\<close>
-
-consts
-  iarg :: \<open>'a\<close> ("{}")
-  hole :: \<open>'b\<close> ("?")
-
-ML_file \<open>implicits.ML\<close>
-
-attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
-
-ML \<open>val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\<close>
-
-text \<open>Automatically insert inhabitation judgments where needed:\<close>
-
-syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
-translations "inhabited A" \<rightharpoonup> "CONST has_type ? A"
-
-
 subsection \<open>Implicit lambdas\<close>
 
 definition lam_i where [implicit]: "lam_i f \<equiv> lam {} f"