aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
authorJosh Chen2020-07-21 19:31:31 +0200
committerJosh Chen2020-07-21 19:31:31 +0200
commit6464ab52b593ceb9d92b9c0c38df32c049537262 (patch)
treee452653b8966d79e1751915544639eb8b3240576 /spartan
parent306721649f0963ab225deb8d5670cfe196bb360d (diff)
minor
Diffstat (limited to 'spartan')
-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>