commit by user mkmluser

[helm.git] / weblib / cicm2012 / reals.ma

diff --git a/weblib/cicm2012/reals.ma b/weblib/cicm2012/reals.ma
new file mode 100644 (file)
index 0000000..4b4b431
--- /dev/null
+++ b/weblib/cicm2012/reals.ma
@@ -0,0 +1,5 @@
+include "basics/logic.ma".
+
+\ 5img class="anchor" src="icons/tick.png" id="R"\ 6axiom R : Type[0].
+\ 5img class="anchor" src="icons/tick.png" id="add"\ 6axiom add : \ 5a href="cic:/matita/cicm2012/reals/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/cicm2012/reals/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/cicm2012/reals/R.dec"\ 6R\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="times"\ 6axiom times : \ 5a href="cic:/matita/cicm2012/reals/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/cicm2012/reals/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/cicm2012/reals/R.dec"\ 6R\ 5/a\ 6.
\ No newline at end of file