diff options
Diffstat (limited to 'Equal.thy')
| -rw-r--r-- | Equal.thy | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -12,13 +12,13 @@ begin section \<open>Constants and syntax\<close> axiomatization - Equal :: "[Term, Term, Term] \<Rightarrow> Term" and - refl :: "Term \<Rightarrow> Term" and - indEqual :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=)") + Equal :: "[t, t, t] \<Rightarrow> t" and + refl :: "t \<Rightarrow> t" and + indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>=)") syntax - "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) - "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 0, 101] 100) + "_EQUAL" :: "[t, t, t] \<Rightarrow> t" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) + "_EQUAL_ASCII" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) translations "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" |