diff options
| author | Josh Chen | 2019-02-28 18:42:59 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-28 18:42:59 +0100 |
| commit | 73e7023a301753e91dfdc9ba49c4bcff91dbddc3 (patch) | |
| tree | 85ff3a1ccf832358d51b27b7f5ccf1d6986fd84f /HoTT_Base.thy | |
| parent | 2116cee735ca505e2eae260f48341a4d8ab24117 (diff) | |
tweak mixfix priorities
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 34474d1..ee36af4 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -66,8 +66,8 @@ where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)" text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close> -abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("^_" [1000]) -where "^A \<equiv> \<lambda>_. A" +abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("&_" [0] 3) +where "&A \<equiv> \<lambda>_. A" section \<open>Named theorems\<close> |