From fd05d5ee6ec6b74a88f1b6f25319760b4c05ba7c Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 5 Oct 2011 12:23:45 +0000 Subject: [PATCH] commit by user utente --- weblib/flagtest/prova.ma | 3 +++ weblib/test.ma | 3 +++ 2 files changed, 6 insertions(+) create mode 100644 weblib/test.ma 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 -- 2.39.2