diff options
| author | Josh Chen | 2018-06-15 17:17:27 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-06-15 17:17:27 +0200 |
| commit | 602ad9fe0e2ed1ad4ab6f16e720de878aadc0fba (patch) | |
| tree | 3882162eff20f5bce4bf85cffe067a0e8475dd08 /HoTT_Theorems.thy | |
| parent | 91efce41a2319a9fb861ff26d7dc8c49ec726d4c (diff) | |
projections
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 |