aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--hott/List_HoTT.thy4
-rw-r--r--mltt/core/MLTT.thy12
-rw-r--r--mltt/core/goals.ML3
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''