manual

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index a592b1377dfc9815c0d4f706193bab46e1218a4f..b735e12100875671f0f1087662810ef86fad2f6a 100644 (file)
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -1116,4 +1116,5 @@ lemma le_maxr: ∀i,n,m. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a
 
 lemma to_max: ∀i,n,m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i.
 #i #n #m #leni #lemi normalize (cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n m)) 
-normalize // qed.
\ No newline at end of file
+normalize // qed.
+

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index a32d67a0a6a8ecfb2157748a853b1517258951a4..bd832f5f9f9d591f787bd8ee4055f09852c4992b 100644 (file)
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -100,14 +100,3 @@ notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp
 definition ite ≝ λA:Type[0].λe.λt,f:A.match e with [ true ⇒ t | false ⇒ f ].
 
 interpretation "if then else" 'ite e t f = (ite ? e t f).
-
-(* axiom foo : ∀b.\ 5a title="if then else" href="cic:/fakeuri.def(1)"\ 6£\ 5/a\ 6 b &amp; \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 &amp; \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. *)
-axiom foo : ∀b. if b then True else False.
-
-(*theorem 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).
-#b1 #b2 (cases b1) (cases b2) /\ 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/ %2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-
-theorem 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.*)
\ No newline at end of file

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index b9dfed28c7d70dc1d39e7ca68fa9b5e533be02de..527e48429836af118c8f812430b6e2e95e6fe855 100644 (file)
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -269,4 +269,4 @@ qed.
 
 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[3].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
  #T #t #P #H #p >(\ 5a href="cic:/matita/basics/logic/lemmaK.def(2)"\ 6lemmaK\ 5/a\ 6 T t p) @H
-qed.
\ No newline at end of file
+qed.