- MatitaMisc: we factorized here the function out_preamble used in matitadep

[helm.git] / helm / software / matita / contribs / procedural / library / preamble.ma

diff --git a/helm/software/matita/contribs/procedural/library/preamble.ma b/helm/software/matita/contribs/procedural/library/preamble.ma
index 5bad8268511dea8b494f6a3dbb965b89ee019603..df40a272fced212c56d373888121d564c41ea4f0 100644 (file)
--- a/helm/software/matita/contribs/procedural/library/preamble.ma
+++ b/helm/software/matita/contribs/procedural/library/preamble.ma
@@ -12,21 +12,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-default "true" cic:/matita/logic/connectives/True.ind.
-
-default "false" cic:/matita/logic/connectives/False.ind.
-
-default "absurd" cic:/matita/logic/connectives/absurd.con.
-
-default "equality"
- cic:/matita/logic/equality/eq.ind
- cic:/matita/logic/equality/sym_eq.con
- cic:/matita/logic/equality/transitive_eq.con
- cic:/matita/logic/equality/eq_ind.con
- cic:/matita/logic/equality/eq_elim_r.con
- cic:/matita/logic/equality/eq_rec.con
- cic:/matita/logic/equality/eq_elim_r'.con
- cic:/matita/logic/equality/eq_rect.con
- cic:/matita/logic/equality/eq_elim_r''.con
- cic:/matita/logic/equality/eq_f.con
- cic:/matita/logic/equality/eq_OF_eq.con.
+include "../../../library/theory.ma".