From: Ferruccio Guidi Date: Wed, 13 Feb 2008 13:40:54 +0000 (+0000) Subject: renaming X-Git-Tag: make_still_working~5610 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb9237a1eb706f8d7e6ed0fea9e6f6a65fa5d7fe;p=helm.git renaming --- diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile index f67b79581..125029529 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile @@ -4,7 +4,7 @@ MMAS = $(shell find -name "*.mma") MAS = $(MMAS:%.mma=%.ma) %.ma: %.mma - echo -e "$< preamble.ma \npreamble.ma" > depends +# echo -e "$< preamble.ma \npreamble.ma" > depends ../../../matitac.opt -dump $@ $< 2>/dev/null ../../../matitadep.opt ../../../matitac.opt $@ @@ -19,8 +19,9 @@ clean: clean.opt: ../../../matitaclean.opt rm -f $(MAS) +depend: + ../../../matitadep +depend.opt: + ../../../matitadep.opt -theory2.ma: theory2.mma ext/tactics2.ma ext/arith2.ma types/props2.ma blt/props2.ma plist/props2.ma -types/props2.ma: types/props2.mma types/defs2.ma -blt/props2.ma: blt/props2.mma blt/defs2.ma -plist/props2.ma: plist/props2.mma plist/defs2.ma +include xdepend diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma new file mode 100644 index 000000000..12438b398 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs". + +include "preamble.ma". + + +(* object blt not inlined *) + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma deleted file mode 100644 index 12438b398..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs". - -include "preamble.ma". - - -(* object blt not inlined *) - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma new file mode 100644 index 000000000..d24466394 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props". + +include "blt/defs.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.con". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma deleted file mode 100644 index d24466394..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props". - -include "blt/defs.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.con". - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma new file mode 100644 index 000000000..0047b1438 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith". + +include "preamble.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma deleted file mode 100644 index 0047b1438..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma +++ /dev/null @@ -1,114 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith". - -include "preamble.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con". - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma new file mode 100644 index 000000000..18de7f71a --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics". + +include "preamble.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma deleted file mode 100644 index 18de7f71a..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics". - -include "preamble.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con". - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma new file mode 100644 index 000000000..3dc03da0b --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs". + +include "preamble.ma". + + +(* object PList not inlined *) + + +(* object PConsTail not inlined *) + + +(* object Ss not inlined *) + + +(* object papp not inlined *) + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma deleted file mode 100644 index 3dc03da0b..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma +++ /dev/null @@ -1,32 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs". - -include "preamble.ma". - - -(* object PList not inlined *) - - -(* object PConsTail not inlined *) - - -(* object Ss not inlined *) - - -(* object papp not inlined *) - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma new file mode 100644 index 000000000..29357a88a --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props". + +include "plist/defs.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma deleted file mode 100644 index 29357a88a..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props". - -include "plist/defs.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma new file mode 100644 index 000000000..1adab3e2b --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory". + +include "ext/tactics.ma". + +include "ext/arith.ma". + +include "types/props.ma". + +include "blt/props.ma". + +include "plist/props.ma". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma deleted file mode 100644 index 1adab3e2b..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory". - -include "ext/tactics.ma". - -include "ext/arith.ma". - -include "types/props.ma". - -include "blt/props.ma". - -include "plist/props.ma". - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma new file mode 100644 index 000000000..87c3378c2 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs". + +include "preamble.ma". + + +(* object and3 not inlined *) + + +(* object and4 not inlined *) + + +(* object and5 not inlined *) + + +(* object or3 not inlined *) + + +(* object or4 not inlined *) + + +(* object ex3 not inlined *) + + +(* object ex4 not inlined *) + + +(* object ex_2 not inlined *) + + +(* object ex2_2 not inlined *) + + +(* object ex3_2 not inlined *) + + +(* object ex4_2 not inlined *) + + +(* object ex_3 not inlined *) + + +(* object ex2_3 not inlined *) + + +(* object ex3_3 not inlined *) + + +(* object ex4_3 not inlined *) + + +(* object ex3_4 not inlined *) + + +(* object ex4_4 not inlined *) + + +(* object ex4_5 not inlined *) + + +(* object ex5_5 not inlined *) + + +(* object ex6_6 not inlined *) + + +(* object ex6_7 not inlined *) + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma deleted file mode 100644 index 87c3378c2..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma +++ /dev/null @@ -1,83 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs". - -include "preamble.ma". - - -(* object and3 not inlined *) - - -(* object and4 not inlined *) - - -(* object and5 not inlined *) - - -(* object or3 not inlined *) - - -(* object or4 not inlined *) - - -(* object ex3 not inlined *) - - -(* object ex4 not inlined *) - - -(* object ex_2 not inlined *) - - -(* object ex2_2 not inlined *) - - -(* object ex3_2 not inlined *) - - -(* object ex4_2 not inlined *) - - -(* object ex_3 not inlined *) - - -(* object ex2_3 not inlined *) - - -(* object ex3_3 not inlined *) - - -(* object ex4_3 not inlined *) - - -(* object ex3_4 not inlined *) - - -(* object ex4_4 not inlined *) - - -(* object ex4_5 not inlined *) - - -(* object ex5_5 not inlined *) - - -(* object ex6_6 not inlined *) - - -(* object ex6_7 not inlined *) - diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma new file mode 100644 index 000000000..d79bfc46b --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props". + +include "types/defs.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma deleted file mode 100644 index d79bfc46b..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props". - -include "types/defs.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". -