aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core')
-rw-r--r--spartan/core/Spartan.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index fa6148f..8c87c2e 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -462,7 +462,7 @@ lemma id_right [comp]:
lemma id_U [typechk]:
"id (U i): U i \<rightarrow> U i"
- by typechk (rule Ui_in_USi) (*FIXME: Add annotation rule to typechecker*)
+ using Ui_in_USi by typechk
section \<open>Pairs\<close>