commit by user utente

diff --git a/weblib/flagtest/prova.ma b/weblib/flagtest/prova.ma
index f14392e9363b16d8b82eea79a35fcc25eafc7ccc..cf8a896676a6d9c7cf704680fa28432c4b10a200 100644 (file)
--- 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. \ 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.
+>>>>>>> .r11514

diff --git a/weblib/test.ma b/weblib/test.ma
new file mode 100644 (file)
index 0000000..362fb6d
--- /dev/null
+++ b/weblib/test.ma
@@ -0,0 +1,3 @@
+(* prova *)
+
+axiom pippo : Prop.
\ No newline at end of file