aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-06-30 17:29:00 +0200
committerJosh Chen2018-06-30 17:29:00 +0200
commitadfb8f33e223049e7e9fa5a279cc4d641fb2466f (patch)
treef59aeea0977ffaacd4d7542b966c32be5a42c9b2
parent352a6e40a5bdf193b8f9690e76aede4e0650a445 (diff)
Fix precedence of =
-rw-r--r--Equal.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Equal.thy b/Equal.thy
index 6c18084..f0ced68 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -18,7 +18,7 @@ axiomatization
section \<open>Syntax\<close>
syntax
- "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100)
+ "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
"_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 0, 101] 100)
translations
"a =[A] b" \<rightleftharpoons> "CONST Equal A a b"