diff options
| -rw-r--r-- | hott/List_HoTT.thy | 4 | ||||
| -rw-r--r-- | mltt/core/MLTT.thy | 12 | ||||
| -rw-r--r-- | mltt/core/goals.ML | 3 |
3 files changed, 11 insertions, 8 deletions
diff --git a/hott/List_HoTT.thy b/hott/List_HoTT.thy index a48d2ab..dc52320 100644 --- a/hott/List_HoTT.thy +++ b/hott/List_HoTT.thy @@ -10,8 +10,8 @@ section \<open>Length\<close> definition [implicit]: "len \<equiv> ListRec {} Nat 0 (fn _ _ rec. suc rec)" experiment begin - Lemma "len [] \<equiv> ?n" by compute - Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by compute + Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)+ + Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+ end diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy index 29c7248..96cbe96 100644 --- a/mltt/core/MLTT.thy +++ b/mltt/core/MLTT.thy @@ -63,15 +63,15 @@ typedecl lvl axiomatization O :: \<open>lvl\<close> and S :: \<open>lvl \<Rightarrow> lvl\<close> and - lt :: \<open>lvl \<Rightarrow> lvl \<Rightarrow> prop\<close> (infix "<" 900) + lt :: \<open>lvl \<Rightarrow> lvl \<Rightarrow> prop\<close> (infix "<\<^sub>U" 900) where - O_min: "O < S i" and - lt_S: "i < S i" and - lt_trans: "i < j \<Longrightarrow> j < k \<Longrightarrow> i < k" + O_min: "O <\<^sub>U S i" and + lt_S: "i <\<^sub>U S i" and + lt_trans: "i <\<^sub>U j \<Longrightarrow> j <\<^sub>U k \<Longrightarrow> i <\<^sub>U k" axiomatization U :: \<open>lvl \<Rightarrow> o\<close> where - Ui_in_Uj: "i < j \<Longrightarrow> U i: U j" and - U_cumul: "A: U i \<Longrightarrow> i < j \<Longrightarrow> A: U j" + Ui_in_Uj: "i <\<^sub>U j \<Longrightarrow> U i: U j" and + U_cumul: "A: U i \<Longrightarrow> i <\<^sub>U j \<Longrightarrow> A: U j" lemma Ui_in_USi: "U i: U (S i)" diff --git a/mltt/core/goals.ML b/mltt/core/goals.ML index 4d03133..23a6c28 100644 --- a/mltt/core/goals.ML +++ b/mltt/core/goals.ML @@ -189,6 +189,9 @@ fun gen_schematic_theorem if defn then single (Proof_Display.print_results do_print pos lthy'' ((kind, Binding.name_of name_def), [("", defs)])) + else if not long andalso not substmts then + single (Proof_Display.print_results do_print pos lthy'' + ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')) else (if long then Proof_Display.print_results do_print pos lthy'' |