diff options
| author | Josh Chen | 2020-07-21 19:31:31 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-21 19:31:31 +0200 |
| commit | 6464ab52b593ceb9d92b9c0c38df32c049537262 (patch) | |
| tree | e452653b8966d79e1751915544639eb8b3240576 | |
| parent | 306721649f0963ab225deb8d5670cfe196bb360d (diff) | |
minor
| -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> |