reverted to previous version (plus anchors)

[helm.git] / weblib / basics / bool.ma

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index d532c3186fdca7ffd11fdd611183db88b228f89e..43f0f8d051a16c388c1599f59ee7c649e24128ff 100644 (file)
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -92,10 +92,9 @@ match b1 with [ true ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6tru
   | false ⇒  match b2 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]].
 
 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]  }.
 
 \ 5img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"\ 6theorem bool_to_decidable_eq: 
   ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (b1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b2).
@@ -104,4 +103,3 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp
 \ 5img class="anchor" src="icons/tick.png" id="true_or_false"\ 6theorem true_or_false:
 ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
 #b (cases b) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-