diff options
Diffstat (limited to 'HoTT_Theorems.thy')
| -rw-r--r-- | HoTT_Theorems.thy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 2c2a31d..ab5374d 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -34,6 +34,9 @@ proof fix a assume "a : A" then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. + + ML_val \<open>@{context} |> Variable.names_of\<close> + qed |