From e10f6cc76602309d92af9c831e755dfa5e593b68 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 12 Oct 2011 13:05:01 +0000 Subject: [PATCH] Administrative commit restoring the repository to the usual shape. --- weblib/basics/logic.ma | 3 +-- weblib/basics/relations.ma | 2 +- weblib/ricciott4/prova.ma | 1 - 3 files changed, 2 insertions(+), 4 deletions(-) delete mode 100644 weblib/ricciott4/prova.ma diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma index 5e97f9b5c..c64f887c6 100644 --- a/weblib/basics/logic.ma +++ b/weblib/basics/logic.ma @@ -223,5 +223,4 @@ definition R4 : qed. (* TODO concrete definition by means of proof irrelevance *) -axiom streicherK : ∀T:Type[1].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[2].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p. - +axiom streicherK : ∀T:Type[1].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[2].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p. \ No newline at end of file diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma index 3081fa96b..34d6fe11c 100644 --- a/weblib/basics/relations.ma +++ b/weblib/basics/relations.ma @@ -102,4 +102,4 @@ notation " f \eqF g " non associative with precedence 45 for @{'eqF ? ? f g}. interpretation "functional extentional equality" -'eqF A B f g = (exteqF A B f g). \ No newline at end of file +'eqF A B f g = (exteqF A B f g). diff --git a/weblib/ricciott4/prova.ma b/weblib/ricciott4/prova.ma deleted file mode 100644 index 9ca5a7e15..000000000 --- a/weblib/ricciott4/prova.ma +++ /dev/null @@ -1 +0,0 @@ -axiom paperino : Prop. \ No newline at end of file -- 2.39.2