aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Equal.thy')
-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"