From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 6 Jul 2012 12:12:46 +0000 (+0000)
Subject: manual
X-Git-Tag: make_still_working~1622
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7f6235dca57343e63217316b6415599daef7d4aa;p=helm.git

manual
---

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index a592b1377..b735e1210 100644
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -1116,4 +1116,5 @@ lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a
 
 lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i.
 #i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a 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 a32d67a0a..bd832f5f9 100644
--- 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.a title="if then else" href="cic:/fakeuri.def(1)"£/a b &amp; a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a &amp; a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. *)
-axiom foo : ∀b. if b then True else False.
-
-(*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).
-#b1 #b2 (cases b1) (cases b2) /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/ %2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ qed.
-
-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.*)
\ No newline at end of file
diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index b9dfed28c..527e48429 100644
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -269,4 +269,4 @@ qed.
 
 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[3].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p.
  #T #t #P #H #p >(a href="cic:/matita/basics/logic/lemmaK.def(2)"lemmaK/a T t p) @H
-qed.
\ No newline at end of file
+qed.