X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fbool.ma;h=43f0f8d051a16c388c1599f59ee7c649e24128ff;hb=80b2ee96ffe418af9c39d3714e2a2f1dc74dab41;hp=d532c3186fdca7ffd11fdd611183db88b228f89e;hpb=4386cd1be69b473dc7e12fbe96e156c8b2de7954;p=helm.git

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index d532c3186..43f0f8d05 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -92,10 +92,9 @@ match b1 with [ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"tru
   | false ⇒  match b2 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ]].
 
 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
-(* notation > "£ term 46 e & term 46 t & term 46 f" non associative with precedence 46 *)
- for @{ 'ite $e $t $f }.
+ for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
 notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
- for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }. 
+ for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
 
 img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"theorem bool_to_decidable_eq: 
   ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (b1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ab2).
@@ -104,4 +103,3 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp
 img class="anchor" src="icons/tick.png" id="true_or_false"theorem true_or_false:
 ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
 #b (cases b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
-