From 6c0d3612ade8f6b837bba4c4804f865827ce2140 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Aug 2009 11:34:48 +0000 Subject: [PATCH] exponentiation should output with \sup not with ^, that is meant to be an input only notation. --- helm/software/matita/core_notation.moo | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 328274bb8..f60496326 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -209,6 +209,8 @@ for @{ 'iff $a $b }. notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70 for @{ 'powerset $A }. +notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 70 +for @{ 'powerset $A }. notation < "hvbox({ ident i | term 19 p })" with precedence 90 for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. -- 2.39.2