From: Wilmer Ricciotti Date: Wed, 5 Oct 2011 12:23:45 +0000 (+0000) Subject: commit by user utente X-Git-Tag: make_still_working~2235 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd05d5ee6ec6b74a88f1b6f25319760b4c05ba7c;p=helm.git commit by user utente --- diff --git a/weblib/flagtest/prova.ma b/weblib/flagtest/prova.ma index f14392e93..cf8a89667 100644 --- a/weblib/flagtest/prova.ma +++ b/weblib/flagtest/prova.ma @@ -1,3 +1,5 @@ +<<<<<<< .mine +(* scriptino *)======= (* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science @@ -1116,3 +1118,4 @@ 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. +>>>>>>> .r11514 diff --git a/weblib/test.ma b/weblib/test.ma new file mode 100644 index 000000000..362fb6d57 --- /dev/null +++ b/weblib/test.ma @@ -0,0 +1,3 @@ +(* prova *) + +axiom pippo : Prop. \ No newline at end of file