diff options
| -rw-r--r-- | spartan/core/Spartan.thy | 2 |
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> |