]> matita.cs.unibo.it Git - helm.git/commit
branch for universe universe-declared
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 22 Apr 2008 16:08:58 +0000 (16:08 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 22 Apr 2008 16:08:58 +0000 (16:08 +0000)
commitf61af501fb4608cc4fb062a0864c774e677f0d76
tree7a10b368e44e6fdd1281ab127f5ed5b3f831d7cc
parent58ae1809c352e71e7b5530dc41e2bfc834e1aef1
branch for universe
1850 files changed:
Makefile [new file with mode: 0644]
Makefile.defs.in [new file with mode: 0644]
components/METAS/meta.helm-acic_content.src [new file with mode: 0644]
components/METAS/meta.helm-acic_procedural.src [new file with mode: 0644]
components/METAS/meta.helm-cic.src [new file with mode: 0644]
components/METAS/meta.helm-cic_acic.src [new file with mode: 0644]
components/METAS/meta.helm-cic_disambiguation.src [new file with mode: 0644]
components/METAS/meta.helm-cic_exportation.src [new file with mode: 0644]
components/METAS/meta.helm-cic_proof_checking.src [new file with mode: 0644]
components/METAS/meta.helm-cic_unification.src [new file with mode: 0644]
components/METAS/meta.helm-content_pres.src [new file with mode: 0644]
components/METAS/meta.helm-extlib.src [new file with mode: 0644]
components/METAS/meta.helm-getter.src [new file with mode: 0644]
components/METAS/meta.helm-grafite.src [new file with mode: 0644]
components/METAS/meta.helm-grafite_engine.src [new file with mode: 0644]
components/METAS/meta.helm-grafite_parser.src [new file with mode: 0644]
components/METAS/meta.helm-hgdome.src [new file with mode: 0644]
components/METAS/meta.helm-hmysql.src [new file with mode: 0644]
components/METAS/meta.helm-lexicon.src [new file with mode: 0644]
components/METAS/meta.helm-library.src [new file with mode: 0644]
components/METAS/meta.helm-logger.src [new file with mode: 0644]
components/METAS/meta.helm-metadata.src [new file with mode: 0644]
components/METAS/meta.helm-ng_kernel.src [new file with mode: 0644]
components/METAS/meta.helm-registry.src [new file with mode: 0644]
components/METAS/meta.helm-syntax_extensions.src [new file with mode: 0644]
components/METAS/meta.helm-tactics.src [new file with mode: 0644]
components/METAS/meta.helm-thread.src [new file with mode: 0644]
components/METAS/meta.helm-tptp_grafite.src [new file with mode: 0644]
components/METAS/meta.helm-urimanager.src [new file with mode: 0644]
components/METAS/meta.helm-whelp.src [new file with mode: 0644]
components/METAS/meta.helm-xml.src [new file with mode: 0644]
components/METAS/meta.helm-xmldiff.src [new file with mode: 0644]
components/Makefile [new file with mode: 0644]
components/Makefile.common [new file with mode: 0644]
components/STATS/clusters.dot [new file with mode: 0644]
components/STATS/daemons.dot [new file with mode: 0644]
components/STATS/deps.patch [new file with mode: 0644]
components/STATS/patch_deps.sh [new file with mode: 0755]
components/acic_content/.depend [new file with mode: 0644]
components/acic_content/.depend.opt [new file with mode: 0644]
components/acic_content/Makefile [new file with mode: 0644]
components/acic_content/acic2astMatcher.ml [new file with mode: 0644]
components/acic_content/acic2astMatcher.mli [new file with mode: 0644]
components/acic_content/acic2content.ml [new file with mode: 0644]
components/acic_content/acic2content.mli [new file with mode: 0644]
components/acic_content/cicNotationEnv.ml [new file with mode: 0644]
components/acic_content/cicNotationEnv.mli [new file with mode: 0644]
components/acic_content/cicNotationPp.ml [new file with mode: 0644]
components/acic_content/cicNotationPp.mli [new file with mode: 0644]
components/acic_content/cicNotationPt.ml [new file with mode: 0644]
components/acic_content/cicNotationUtil.ml [new file with mode: 0644]
components/acic_content/cicNotationUtil.mli [new file with mode: 0644]
components/acic_content/content.ml [new file with mode: 0644]
components/acic_content/content.mli [new file with mode: 0644]
components/acic_content/content2cic.ml [new file with mode: 0644]
components/acic_content/content2cic.mli [new file with mode: 0644]
components/acic_content/termAcicContent.ml [new file with mode: 0644]
components/acic_content/termAcicContent.mli [new file with mode: 0644]
components/acic_procedural/.depend [new file with mode: 0644]
components/acic_procedural/.depend.opt [new file with mode: 0644]
components/acic_procedural/Makefile [new file with mode: 0644]
components/acic_procedural/acic2Procedural.ml [new file with mode: 0644]
components/acic_procedural/acic2Procedural.mli [new file with mode: 0644]
components/acic_procedural/proceduralClassify.ml [new file with mode: 0644]
components/acic_procedural/proceduralClassify.mli [new file with mode: 0644]
components/acic_procedural/proceduralConversion.ml [new file with mode: 0644]
components/acic_procedural/proceduralConversion.mli [new file with mode: 0644]
components/acic_procedural/proceduralHelpers.ml [new file with mode: 0644]
components/acic_procedural/proceduralHelpers.mli [new file with mode: 0644]
components/acic_procedural/proceduralMode.ml [new file with mode: 0644]
components/acic_procedural/proceduralMode.mli [new file with mode: 0644]
components/acic_procedural/proceduralOptimizer.ml [new file with mode: 0644]
components/acic_procedural/proceduralOptimizer.mli [new file with mode: 0644]
components/acic_procedural/proceduralTypes.ml [new file with mode: 0644]
components/acic_procedural/proceduralTypes.mli [new file with mode: 0644]
components/binaries/Makefile [new file with mode: 0644]
components/binaries/dump_db/dump.sh [new file with mode: 0755]
components/binaries/extractor/.depend [new file with mode: 0644]
components/binaries/extractor/.depend.opt [new file with mode: 0644]
components/binaries/extractor/Makefile [new file with mode: 0644]
components/binaries/extractor/extractor.conf.xml [new file with mode: 0644]
components/binaries/extractor/extractor.ml [new file with mode: 0644]
components/binaries/extractor/extractor_manager.ml [new file with mode: 0644]
components/binaries/heights/.depend [new file with mode: 0644]
components/binaries/heights/.depend.opt [new file with mode: 0644]
components/binaries/heights/Makefile [new file with mode: 0644]
components/binaries/heights/heights.conf.xml [new file with mode: 0644]
components/binaries/heights/heights.ml [new file with mode: 0644]
components/binaries/saturate/Makefile [new file with mode: 0644]
components/binaries/saturate/saturate_main.ml [new file with mode: 0644]
components/binaries/table_creator/.depend [new file with mode: 0644]
components/binaries/table_creator/.depend.opt [new file with mode: 0644]
components/binaries/table_creator/Makefile [new file with mode: 0644]
components/binaries/table_creator/sync_db.sh [new file with mode: 0755]
components/binaries/table_creator/table_creator.ml [new file with mode: 0644]
components/binaries/transcript/.depend [new file with mode: 0644]
components/binaries/transcript/.depend.opt [new file with mode: 0644]
components/binaries/transcript/CoRN.conf.xml [new file with mode: 0644]
components/binaries/transcript/Makefile [new file with mode: 0644]
components/binaries/transcript/engine.ml [new file with mode: 0644]
components/binaries/transcript/engine.mli [new file with mode: 0644]
components/binaries/transcript/grafite.ml [new file with mode: 0644]
components/binaries/transcript/grafite.mli [new file with mode: 0644]
components/binaries/transcript/top.ml [new file with mode: 0644]
components/binaries/transcript/transcript.conf.xml [new file with mode: 0644]
components/binaries/transcript/types.ml [new file with mode: 0644]
components/binaries/transcript/v8Lexer.mll [new file with mode: 0644]
components/binaries/transcript/v8Parser.mly [new file with mode: 0644]
components/binaries/utilities/.depend [new file with mode: 0644]
components/binaries/utilities/.depend.opt [new file with mode: 0644]
components/binaries/utilities/Makefile [new file with mode: 0644]
components/binaries/utilities/create_environment.ml [new file with mode: 0644]
components/binaries/utilities/list_uris.ml [new file with mode: 0644]
components/binaries/utilities/parse_library.ml [new file with mode: 0644]
components/binaries/utilities/test_library.ml [new file with mode: 0644]
components/binaries/utilities/test_xml_parser.ml [new file with mode: 0644]
components/cic/.depend [new file with mode: 0644]
components/cic/.depend.opt [new file with mode: 0644]
components/cic/Makefile [new file with mode: 0644]
components/cic/cic.ml [new file with mode: 0644]
components/cic/cicInspect.ml [new file with mode: 0644]
components/cic/cicInspect.mli [new file with mode: 0644]
components/cic/cicParser.ml [new file with mode: 0644]
components/cic/cicParser.mli [new file with mode: 0644]
components/cic/cicUniv.ml [new file with mode: 0644]
components/cic/cicUniv.mli [new file with mode: 0644]
components/cic/cicUtil.ml [new file with mode: 0644]
components/cic/cicUtil.mli [new file with mode: 0644]
components/cic/deannotate.ml [new file with mode: 0644]
components/cic/deannotate.mli [new file with mode: 0644]
components/cic/discrimination_tree.ml [new file with mode: 0644]
components/cic/discrimination_tree.mli [new file with mode: 0644]
components/cic/helmLibraryObjects.ml [new file with mode: 0644]
components/cic/helmLibraryObjects.mli [new file with mode: 0644]
components/cic/libraryObjects.ml [new file with mode: 0644]
components/cic/libraryObjects.mli [new file with mode: 0644]
components/cic/path_indexing.ml [new file with mode: 0644]
components/cic/path_indexing.mli [new file with mode: 0644]
components/cic/unshare.ml [new file with mode: 0644]
components/cic/unshare.mli [new file with mode: 0644]
components/cic_acic/.depend [new file with mode: 0644]
components/cic_acic/.depend.opt [new file with mode: 0644]
components/cic_acic/Makefile [new file with mode: 0644]
components/cic_acic/cic2Xml.ml [new file with mode: 0644]
components/cic_acic/cic2Xml.mli [new file with mode: 0644]
components/cic_acic/cic2acic.ml [new file with mode: 0644]
components/cic_acic/cic2acic.mli [new file with mode: 0644]
components/cic_acic/doubleTypeInference.ml [new file with mode: 0644]
components/cic_acic/doubleTypeInference.mli [new file with mode: 0644]
components/cic_acic/eta_fixing.ml [new file with mode: 0644]
components/cic_acic/eta_fixing.mli [new file with mode: 0644]
components/cic_disambiguation/.depend [new file with mode: 0644]
components/cic_disambiguation/.depend.opt [new file with mode: 0644]
components/cic_disambiguation/Makefile [new file with mode: 0644]
components/cic_disambiguation/disambiguate.crit2.ml [new file with mode: 0644]
components/cic_disambiguation/disambiguate.crit4.ml [new file with mode: 0644]
components/cic_disambiguation/disambiguate.ml [new file with mode: 0644]
components/cic_disambiguation/disambiguate.mli [new file with mode: 0644]
components/cic_disambiguation/disambiguateChoices.ml [new file with mode: 0644]
components/cic_disambiguation/disambiguateChoices.mli [new file with mode: 0644]
components/cic_disambiguation/disambiguateTypes.ml [new file with mode: 0644]
components/cic_disambiguation/disambiguateTypes.mli [new file with mode: 0644]
components/cic_disambiguation/doc/precedence.txt [new file with mode: 0644]
components/cic_disambiguation/number_notation.ml [new file with mode: 0644]
components/cic_disambiguation/tests/aliases.txt [new file with mode: 0644]
components/cic_disambiguation/tests/eq.txt [new file with mode: 0644]
components/cic_disambiguation/tests/match.txt [new file with mode: 0644]
components/cic_exportation/.depend [new file with mode: 0644]
components/cic_exportation/.depend.opt [new file with mode: 0644]
components/cic_exportation/Makefile [new file with mode: 0644]
components/cic_exportation/cicExportation.ml [new file with mode: 0644]
components/cic_exportation/cicExportation.mli [new file with mode: 0644]
components/cic_proof_checking/.depend [new file with mode: 0644]
components/cic_proof_checking/.depend.opt [new file with mode: 0644]
components/cic_proof_checking/Makefile [new file with mode: 0644]
components/cic_proof_checking/cicEnvironment.ml [new file with mode: 0644]
components/cic_proof_checking/cicEnvironment.mli [new file with mode: 0644]
components/cic_proof_checking/cicLogger.ml [new file with mode: 0644]
components/cic_proof_checking/cicLogger.mli [new file with mode: 0644]
components/cic_proof_checking/cicMiniReduction.ml [new file with mode: 0644]
components/cic_proof_checking/cicMiniReduction.mli [new file with mode: 0644]
components/cic_proof_checking/cicPp.ml [new file with mode: 0644]
components/cic_proof_checking/cicPp.mli [new file with mode: 0644]
components/cic_proof_checking/cicReduction.ml [new file with mode: 0644]
components/cic_proof_checking/cicReduction.mli [new file with mode: 0644]
components/cic_proof_checking/cicSubstitution.ml [new file with mode: 0644]
components/cic_proof_checking/cicSubstitution.mli [new file with mode: 0644]
components/cic_proof_checking/cicTypeChecker.ml [new file with mode: 0644]
components/cic_proof_checking/cicTypeChecker.mli [new file with mode: 0644]
components/cic_proof_checking/cicUnivUtils.ml [new file with mode: 0644]
components/cic_proof_checking/cicUnivUtils.mli [new file with mode: 0644]
components/cic_proof_checking/doc/inductive.txt [new file with mode: 0644]
components/cic_proof_checking/freshNamesGenerator.ml [new file with mode: 0755]
components/cic_proof_checking/freshNamesGenerator.mli [new file with mode: 0644]
components/cic_unification/.depend [new file with mode: 0644]
components/cic_unification/.depend.opt [new file with mode: 0644]
components/cic_unification/Makefile [new file with mode: 0644]
components/cic_unification/cicMetaSubst.ml [new file with mode: 0644]
components/cic_unification/cicMetaSubst.mli [new file with mode: 0644]
components/cic_unification/cicMkImplicit.ml [new file with mode: 0644]
components/cic_unification/cicMkImplicit.mli [new file with mode: 0644]
components/cic_unification/cicRefine.ml [new file with mode: 0644]
components/cic_unification/cicRefine.mli [new file with mode: 0644]
components/cic_unification/cicReplace.ml [new file with mode: 0644]
components/cic_unification/cicReplace.mli [new file with mode: 0644]
components/cic_unification/cicUnification.ml [new file with mode: 0644]
components/cic_unification/cicUnification.mli [new file with mode: 0644]
components/cic_unification/coercGraph.ml [new file with mode: 0644]
components/cic_unification/coercGraph.mli [new file with mode: 0644]
components/cic_unification/termUtil.ml [new file with mode: 0644]
components/cic_unification/termUtil.mli [new file with mode: 0644]
components/content_pres/.depend [new file with mode: 0644]
components/content_pres/.depend.opt [new file with mode: 0644]
components/content_pres/Makefile [new file with mode: 0644]
components/content_pres/box.ml [new file with mode: 0644]
components/content_pres/box.mli [new file with mode: 0644]
components/content_pres/boxPp.ml [new file with mode: 0644]
components/content_pres/boxPp.mli [new file with mode: 0644]
components/content_pres/cicNotationLexer.ml [new file with mode: 0644]
components/content_pres/cicNotationLexer.mli [new file with mode: 0644]
components/content_pres/cicNotationParser.ml [new file with mode: 0644]
components/content_pres/cicNotationParser.mli [new file with mode: 0644]
components/content_pres/cicNotationPres.ml [new file with mode: 0644]
components/content_pres/cicNotationPres.mli [new file with mode: 0644]
components/content_pres/content2pres.ml [new file with mode: 0644]
components/content_pres/content2pres.mli [new file with mode: 0644]
components/content_pres/content2presMatcher.ml [new file with mode: 0644]
components/content_pres/content2presMatcher.mli [new file with mode: 0644]
components/content_pres/mpresentation.ml [new file with mode: 0644]
components/content_pres/mpresentation.mli [new file with mode: 0644]
components/content_pres/renderingAttrs.ml [new file with mode: 0644]
components/content_pres/renderingAttrs.mli [new file with mode: 0644]
components/content_pres/sequent2pres.ml [new file with mode: 0644]
components/content_pres/sequent2pres.mli [new file with mode: 0644]
components/content_pres/termContentPres.ml [new file with mode: 0644]
components/content_pres/termContentPres.mli [new file with mode: 0644]
components/content_pres/test_lexer.ml [new file with mode: 0644]
components/extlib/.depend [new file with mode: 0644]
components/extlib/.depend.opt [new file with mode: 0644]
components/extlib/Makefile [new file with mode: 0644]
components/extlib/componentsConf.ml.in [new file with mode: 0644]
components/extlib/componentsConf.mli [new file with mode: 0644]
components/extlib/graphvizPp.ml [new file with mode: 0644]
components/extlib/graphvizPp.mli [new file with mode: 0644]
components/extlib/hExtlib.ml [new file with mode: 0644]
components/extlib/hExtlib.mli [new file with mode: 0644]
components/extlib/hLog.ml [new file with mode: 0644]
components/extlib/hLog.mli [new file with mode: 0644]
components/extlib/hMarshal.ml [new file with mode: 0644]
components/extlib/hMarshal.mli [new file with mode: 0644]
components/extlib/hTopoSort.ml [new file with mode: 0644]
components/extlib/hTopoSort.mli [new file with mode: 0644]
components/extlib/patternMatcher.ml [new file with mode: 0644]
components/extlib/patternMatcher.mli [new file with mode: 0644]
components/extlib/refCounter.ml [new file with mode: 0644]
components/extlib/refCounter.mli [new file with mode: 0644]
components/extlib/trie.ml [new file with mode: 0644]
components/extlib/trie.mli [new file with mode: 0644]
components/getter/.depend [new file with mode: 0644]
components/getter/.depend.opt [new file with mode: 0644]
components/getter/.ocamlinit [new file with mode: 0644]
components/getter/Makefile [new file with mode: 0644]
components/getter/http_getter.ml [new file with mode: 0644]
components/getter/http_getter.mli [new file with mode: 0644]
components/getter/http_getter_common.ml [new file with mode: 0644]
components/getter/http_getter_common.mli [new file with mode: 0644]
components/getter/http_getter_const.ml [new file with mode: 0644]
components/getter/http_getter_const.mli [new file with mode: 0644]
components/getter/http_getter_env.ml [new file with mode: 0644]
components/getter/http_getter_env.mli [new file with mode: 0644]
components/getter/http_getter_logger.ml [new file with mode: 0644]
components/getter/http_getter_logger.mli [new file with mode: 0644]
components/getter/http_getter_misc.ml [new file with mode: 0644]
components/getter/http_getter_misc.mli [new file with mode: 0644]
components/getter/http_getter_storage.ml [new file with mode: 0644]
components/getter/http_getter_storage.mli [new file with mode: 0644]
components/getter/http_getter_types.ml [new file with mode: 0644]
components/getter/http_getter_wget.ml [new file with mode: 0644]
components/getter/http_getter_wget.mli [new file with mode: 0644]
components/getter/mkindexes.pl [new file with mode: 0755]
components/getter/sample.conf.xml [new file with mode: 0644]
components/getter/test.ml [new file with mode: 0644]
components/grafite/.depend [new file with mode: 0644]
components/grafite/.depend.opt [new file with mode: 0644]
components/grafite/Makefile [new file with mode: 0644]
components/grafite/grafiteAst.ml [new file with mode: 0644]
components/grafite/grafiteAstPp.ml [new file with mode: 0644]
components/grafite/grafiteAstPp.mli [new file with mode: 0644]
components/grafite/grafiteMarshal.ml [new file with mode: 0644]
components/grafite/grafiteMarshal.mli [new file with mode: 0644]
components/grafite_engine/.depend [new file with mode: 0644]
components/grafite_engine/.depend.opt [new file with mode: 0644]
components/grafite_engine/Makefile [new file with mode: 0644]
components/grafite_engine/grafiteEngine.ml [new file with mode: 0644]
components/grafite_engine/grafiteEngine.mli [new file with mode: 0644]
components/grafite_engine/grafiteSync.ml [new file with mode: 0644]
components/grafite_engine/grafiteSync.mli [new file with mode: 0644]
components/grafite_engine/grafiteTypes.ml [new file with mode: 0644]
components/grafite_engine/grafiteTypes.mli [new file with mode: 0644]
components/grafite_parser/.depend [new file with mode: 0644]
components/grafite_parser/.depend.opt [new file with mode: 0644]
components/grafite_parser/Makefile [new file with mode: 0644]
components/grafite_parser/cicNotation2.ml [new file with mode: 0644]
components/grafite_parser/cicNotation2.mli [new file with mode: 0644]
components/grafite_parser/dependenciesParser.ml [new file with mode: 0644]
components/grafite_parser/dependenciesParser.mli [new file with mode: 0644]
components/grafite_parser/grafiteDisambiguate.ml [new file with mode: 0644]
components/grafite_parser/grafiteDisambiguate.mli [new file with mode: 0644]
components/grafite_parser/grafiteDisambiguator.ml [new file with mode: 0644]
components/grafite_parser/grafiteDisambiguator.mli [new file with mode: 0644]
components/grafite_parser/grafiteParser.ml [new file with mode: 0644]
components/grafite_parser/grafiteParser.mli [new file with mode: 0644]
components/grafite_parser/grafiteWalker.ml [new file with mode: 0644]
components/grafite_parser/grafiteWalker.mli [new file with mode: 0644]
components/grafite_parser/print_grammar.ml [new file with mode: 0644]
components/grafite_parser/test_dep.ml [new file with mode: 0644]
components/grafite_parser/test_parser.ml [new file with mode: 0644]
components/hbugs/.depend [new file with mode: 0644]
components/hbugs/Makefile [new file with mode: 0644]
components/hbugs/broker.ml [new file with mode: 0644]
components/hbugs/client.ml [new file with mode: 0644]
components/hbugs/data/hbugs_tutor.TPL.ml [new file with mode: 0644]
components/hbugs/data/tutors_index.xml [new file with mode: 0644]
components/hbugs/doc/hbugs.dia [new file with mode: 0644]
components/hbugs/hbugs_broker_registry.ml [new file with mode: 0644]
components/hbugs/hbugs_broker_registry.mli [new file with mode: 0644]
components/hbugs/hbugs_client.ml [new file with mode: 0644]
components/hbugs/hbugs_client.mli [new file with mode: 0644]
components/hbugs/hbugs_client_gui.glade [new file with mode: 0644]
components/hbugs/hbugs_common.ml [new file with mode: 0644]
components/hbugs/hbugs_common.mli [new file with mode: 0644]
components/hbugs/hbugs_id_generator.ml [new file with mode: 0644]
components/hbugs/hbugs_id_generator.mli [new file with mode: 0644]
components/hbugs/hbugs_messages.ml [new file with mode: 0644]
components/hbugs/hbugs_messages.mli [new file with mode: 0644]
components/hbugs/hbugs_misc.ml [new file with mode: 0644]
components/hbugs/hbugs_misc.mli [new file with mode: 0644]
components/hbugs/hbugs_tutors.ml [new file with mode: 0644]
components/hbugs/hbugs_tutors.mli [new file with mode: 0644]
components/hbugs/hbugs_types.mli [new file with mode: 0644]
components/hbugs/scripts/brokerctl.sh [new file with mode: 0755]
components/hbugs/scripts/build_tutors.ml [new file with mode: 0755]
components/hbugs/scripts/ls_tutors.ml [new file with mode: 0755]
components/hbugs/scripts/sabba.sh [new file with mode: 0755]
components/hbugs/search_pattern_apply_tutor.ml [new file with mode: 0644]
components/hbugs/test/HBUGS_MESSAGES.xml [new file with mode: 0644]
components/hbugs/test/Makefile [new file with mode: 0644]
components/hbugs/test/test_serialization.ml [new file with mode: 0644]
components/hgdome/.depend [new file with mode: 0644]
components/hgdome/.depend.opt [new file with mode: 0644]
components/hgdome/Makefile [new file with mode: 0644]
components/hgdome/domMisc.ml [new file with mode: 0644]
components/hgdome/domMisc.mli [new file with mode: 0644]
components/hgdome/xml2Gdome.ml [new file with mode: 0644]
components/hgdome/xml2Gdome.mli [new file with mode: 0644]
components/hmysql/.depend [new file with mode: 0644]
components/hmysql/.depend.opt [new file with mode: 0644]
components/hmysql/Makefile [new file with mode: 0644]
components/hmysql/hMysql.ml [new file with mode: 0644]
components/hmysql/hSql.ml [new file with mode: 0644]
components/hmysql/hSql.mli [new file with mode: 0644]
components/hmysql/hSqlite3.ml [new file with mode: 0644]
components/lexicon/.depend [new file with mode: 0644]
components/lexicon/.depend.opt [new file with mode: 0644]
components/lexicon/Makefile [new file with mode: 0644]
components/lexicon/cicNotation.ml [new file with mode: 0644]
components/lexicon/cicNotation.mli [new file with mode: 0644]
components/lexicon/disambiguatePp.ml [new file with mode: 0644]
components/lexicon/disambiguatePp.mli [new file with mode: 0644]
components/lexicon/lexiconAst.ml [new file with mode: 0644]
components/lexicon/lexiconAstPp.ml [new file with mode: 0644]
components/lexicon/lexiconAstPp.mli [new file with mode: 0644]
components/lexicon/lexiconEngine.ml [new file with mode: 0644]
components/lexicon/lexiconEngine.mli [new file with mode: 0644]
components/lexicon/lexiconMarshal.ml [new file with mode: 0644]
components/lexicon/lexiconMarshal.mli [new file with mode: 0644]
components/lexicon/lexiconSync.ml [new file with mode: 0644]
components/lexicon/lexiconSync.mli [new file with mode: 0644]
components/library/.depend [new file with mode: 0644]
components/library/.depend.opt [new file with mode: 0644]
components/library/Makefile [new file with mode: 0644]
components/library/cicCoercion.ml [new file with mode: 0644]
components/library/cicCoercion.mli [new file with mode: 0644]
components/library/cicElim.ml [new file with mode: 0644]
components/library/cicElim.mli [new file with mode: 0644]
components/library/cicRecord.ml [new file with mode: 0644]
components/library/cicRecord.mli [new file with mode: 0644]
components/library/coercDb.ml [new file with mode: 0644]
components/library/coercDb.mli [new file with mode: 0644]
components/library/librarian.ml [new file with mode: 0644]
components/library/librarian.mli [new file with mode: 0644]
components/library/libraryClean.ml [new file with mode: 0644]
components/library/libraryClean.mli [new file with mode: 0644]
components/library/libraryDb.ml [new file with mode: 0644]
components/library/libraryDb.mli [new file with mode: 0644]
components/library/libraryMisc.ml [new file with mode: 0644]
components/library/libraryMisc.mli [new file with mode: 0644]
components/library/librarySync.ml [new file with mode: 0644]
components/library/librarySync.mli [new file with mode: 0644]
components/library/refinementTool.ml [new file with mode: 0644]
components/license [new file with mode: 0644]
components/logger/.depend [new file with mode: 0644]
components/logger/.depend.opt [new file with mode: 0644]
components/logger/Makefile [new file with mode: 0644]
components/logger/helmLogger.ml [new file with mode: 0644]
components/logger/helmLogger.mli [new file with mode: 0644]
components/metadata/.depend [new file with mode: 0644]
components/metadata/.depend.opt [new file with mode: 0644]
components/metadata/Makefile [new file with mode: 0644]
components/metadata/metadataConstraints.ml [new file with mode: 0644]
components/metadata/metadataConstraints.mli [new file with mode: 0644]
components/metadata/metadataDb.ml [new file with mode: 0644]
components/metadata/metadataDb.mli [new file with mode: 0644]
components/metadata/metadataDeps.ml [new file with mode: 0644]
components/metadata/metadataDeps.mli [new file with mode: 0644]
components/metadata/metadataExtractor.ml [new file with mode: 0644]
components/metadata/metadataExtractor.mli [new file with mode: 0644]
components/metadata/metadataPp.ml [new file with mode: 0644]
components/metadata/metadataPp.mli [new file with mode: 0644]
components/metadata/metadataTypes.ml [new file with mode: 0644]
components/metadata/metadataTypes.mli [new file with mode: 0644]
components/metadata/sqlStatements.ml [new file with mode: 0644]
components/metadata/sqlStatements.mli [new file with mode: 0644]
components/ng_kernel/.depend [new file with mode: 0644]
components/ng_kernel/.depend.opt [new file with mode: 0644]
components/ng_kernel/Makefile [new file with mode: 0644]
components/ng_kernel/alluris.txt [new file with mode: 0644]
components/ng_kernel/check.ml [new file with mode: 0644]
components/ng_kernel/nCic.ml [new file with mode: 0644]
components/ng_kernel/nCic2OCic.ml [new file with mode: 0644]
components/ng_kernel/nCic2OCic.mli [new file with mode: 0644]
components/ng_kernel/nCicEnvironment.ml [new file with mode: 0644]
components/ng_kernel/nCicEnvironment.mli [new file with mode: 0644]
components/ng_kernel/nCicPp.ml [new file with mode: 0644]
components/ng_kernel/nCicPp.mli [new file with mode: 0644]
components/ng_kernel/nCicReduction.ml [new file with mode: 0644]
components/ng_kernel/nCicReduction.mli [new file with mode: 0644]
components/ng_kernel/nCicSubstitution.ml [new file with mode: 0644]
components/ng_kernel/nCicSubstitution.mli [new file with mode: 0644]
components/ng_kernel/nCicTypeChecker.ml [new file with mode: 0644]
components/ng_kernel/nCicTypeChecker.mli [new file with mode: 0644]
components/ng_kernel/nCicUtils.ml [new file with mode: 0644]
components/ng_kernel/nCicUtils.mli [new file with mode: 0644]
components/ng_kernel/nReference.ml [new file with mode: 0644]
components/ng_kernel/nReference.mli [new file with mode: 0644]
components/ng_kernel/nUri.ml [new file with mode: 0644]
components/ng_kernel/nUri.mli [new file with mode: 0644]
components/ng_kernel/oCic2NCic.ml [new file with mode: 0644]
components/ng_kernel/oCic2NCic.mli [new file with mode: 0644]
components/ng_kernel/rt.ml [new file with mode: 0644]
components/ng_kernel/test.ma [new file with mode: 0644]
components/registry/.depend [new file with mode: 0644]
components/registry/.depend.opt [new file with mode: 0644]
components/registry/.ocamlinit [new file with mode: 0644]
components/registry/Makefile [new file with mode: 0644]
components/registry/helm_registry.ml [new file with mode: 0644]
components/registry/helm_registry.mli [new file with mode: 0644]
components/registry/test.ml [new file with mode: 0644]
components/registry/tests/sample.xml [new file with mode: 0644]
components/registry/tests/sample_include.xml [new file with mode: 0644]
components/syntax_extensions/.depend [new file with mode: 0644]
components/syntax_extensions/.depend.opt [new file with mode: 0644]
components/syntax_extensions/Makefile [new file with mode: 0644]
components/syntax_extensions/README.syntax [new file with mode: 0644]
components/syntax_extensions/data/dictionary-tex.xml [new file with mode: 0644]
components/syntax_extensions/data/entities-table.xml [new file with mode: 0644]
components/syntax_extensions/data/extra-entities.xml [new file with mode: 0644]
components/syntax_extensions/make_table.ml [new file with mode: 0644]
components/syntax_extensions/pa_unicode_macro.ml [new file with mode: 0644]
components/syntax_extensions/profiling_macros.ml [new file with mode: 0644]
components/syntax_extensions/test.ml [new file with mode: 0644]
components/syntax_extensions/utf8Macro.ml [new file with mode: 0644]
components/syntax_extensions/utf8Macro.mli [new file with mode: 0644]
components/syntax_extensions/utf8MacroTable.ml [new file with mode: 0644]
components/syntax_extensions/utf8MacroTable.ml.txt [new file with mode: 0644]
components/tactics/.depend [new file with mode: 0644]
components/tactics/.depend.opt [new file with mode: 0644]
components/tactics/Makefile [new file with mode: 0644]
components/tactics/auto.ml [new file with mode: 0644]
components/tactics/auto.mli [new file with mode: 0644]
components/tactics/autoCache.ml [new file with mode: 0644]
components/tactics/autoCache.mli [new file with mode: 0644]
components/tactics/autoTypes.ml [new file with mode: 0644]
components/tactics/autoTypes.mli [new file with mode: 0644]
components/tactics/closeCoercionGraph.ml [new file with mode: 0644]
components/tactics/closeCoercionGraph.mli [new file with mode: 0644]
components/tactics/compose.ml [new file with mode: 0644]
components/tactics/compose.mli [new file with mode: 0644]
components/tactics/continuationals.ml [new file with mode: 0644]
components/tactics/continuationals.mli [new file with mode: 0644]
components/tactics/declarative.ml [new file with mode: 0644]
components/tactics/declarative.mli [new file with mode: 0644]
components/tactics/destructTactic.ml [new file with mode: 0644]
components/tactics/destructTactic.mli [new file with mode: 0644]
components/tactics/doc/Makefile [new file with mode: 0644]
components/tactics/doc/body.tex [new file with mode: 0644]
components/tactics/doc/infernce.sty [new file with mode: 0644]
components/tactics/doc/ligature.sty [new file with mode: 0644]
components/tactics/doc/main.tex [new file with mode: 0644]
components/tactics/doc/reserved.sty [new file with mode: 0644]
components/tactics/doc/semantic.sty [new file with mode: 0644]
components/tactics/doc/shrthand.sty [new file with mode: 0644]
components/tactics/doc/tdiagram.sty [new file with mode: 0644]
components/tactics/eliminationTactics.ml [new file with mode: 0644]
components/tactics/eliminationTactics.mli [new file with mode: 0644]
components/tactics/equalityTactics.ml [new file with mode: 0644]
components/tactics/equalityTactics.mli [new file with mode: 0644]
components/tactics/fourier.ml [new file with mode: 0644]
components/tactics/fourier.mli [new file with mode: 0644]
components/tactics/fourierR.ml [new file with mode: 0644]
components/tactics/fourierR.mli [new file with mode: 0644]
components/tactics/fwdSimplTactic.ml [new file with mode: 0644]
components/tactics/fwdSimplTactic.mli [new file with mode: 0644]
components/tactics/hashtbl_equiv.ml [new file with mode: 0644]
components/tactics/hashtbl_equiv.mli [new file with mode: 0644]
components/tactics/history.ml [new file with mode: 0644]
components/tactics/history.mli [new file with mode: 0644]
components/tactics/introductionTactics.ml [new file with mode: 0644]
components/tactics/introductionTactics.mli [new file with mode: 0644]
components/tactics/inversion.ml [new file with mode: 0644]
components/tactics/inversion.mli [new file with mode: 0644]
components/tactics/inversion_principle.ml [new file with mode: 0644]
components/tactics/inversion_principle.mli [new file with mode: 0644]
components/tactics/metadataQuery.ml [new file with mode: 0644]
components/tactics/metadataQuery.mli [new file with mode: 0644]
components/tactics/negationTactics.ml [new file with mode: 0644]
components/tactics/negationTactics.mli [new file with mode: 0644]
components/tactics/paramodulation/.depend [new file with mode: 0644]
components/tactics/paramodulation/Makefile [new file with mode: 0644]
components/tactics/paramodulation/README [new file with mode: 0644]
components/tactics/paramodulation/equality.ml [new file with mode: 0644]
components/tactics/paramodulation/equality.mli [new file with mode: 0644]
components/tactics/paramodulation/equality_indexing.ml [new file with mode: 0644]
components/tactics/paramodulation/equality_indexing.mli [new file with mode: 0644]
components/tactics/paramodulation/founif.ml [new file with mode: 0644]
components/tactics/paramodulation/founif.mli [new file with mode: 0644]
components/tactics/paramodulation/indexing.ml [new file with mode: 0644]
components/tactics/paramodulation/indexing.mli [new file with mode: 0644]
components/tactics/paramodulation/saturation.ml [new file with mode: 0644]
components/tactics/paramodulation/saturation.mli [new file with mode: 0644]
components/tactics/paramodulation/subst.ml [new file with mode: 0644]
components/tactics/paramodulation/subst.mli [new file with mode: 0644]
components/tactics/paramodulation/test_indexing.ml [new file with mode: 0644]
components/tactics/paramodulation/utils.ml [new file with mode: 0644]
components/tactics/paramodulation/utils.mli [new file with mode: 0644]
components/tactics/primitiveTactics.ml [new file with mode: 0644]
components/tactics/primitiveTactics.mli [new file with mode: 0644]
components/tactics/proofEngineHelpers.ml [new file with mode: 0644]
components/tactics/proofEngineHelpers.mli [new file with mode: 0644]
components/tactics/proofEngineReduction.ml [new file with mode: 0644]
components/tactics/proofEngineReduction.mli [new file with mode: 0644]
components/tactics/proofEngineStructuralRules.ml [new file with mode: 0644]
components/tactics/proofEngineStructuralRules.mli [new file with mode: 0644]
components/tactics/proofEngineTypes.ml [new file with mode: 0644]
components/tactics/proofEngineTypes.mli [new file with mode: 0644]
components/tactics/reductionTactics.ml [new file with mode: 0644]
components/tactics/reductionTactics.mli [new file with mode: 0644]
components/tactics/ring.ml [new file with mode: 0644]
components/tactics/ring.mli [new file with mode: 0644]
components/tactics/setoids.ml [new file with mode: 0644]
components/tactics/setoids.mli [new file with mode: 0644]
components/tactics/statefulProofEngine.ml [new file with mode: 0644]
components/tactics/statefulProofEngine.mli [new file with mode: 0644]
components/tactics/tacticChaser.ml [new file with mode: 0644]
components/tactics/tacticals.ml [new file with mode: 0644]
components/tactics/tacticals.mli [new file with mode: 0644]
components/tactics/tactics.ml [new file with mode: 0644]
components/tactics/tactics.mli [new file with mode: 0644]
components/tactics/universe.ml [new file with mode: 0644]
components/tactics/universe.mli [new file with mode: 0644]
components/tactics/variousTactics.ml [new file with mode: 0644]
components/tactics/variousTactics.mli [new file with mode: 0644]
components/thread/.depend [new file with mode: 0644]
components/thread/.depend.opt [new file with mode: 0644]
components/thread/Makefile [new file with mode: 0644]
components/thread/extThread.ml [new file with mode: 0644]
components/thread/extThread.mli [new file with mode: 0644]
components/thread/fake/threadSafe.ml [new file with mode: 0644]
components/thread/fake/threadSafe.mli [new file with mode: 0644]
components/thread/threadSafe.ml [new file with mode: 0644]
components/thread/threadSafe.mli [new file with mode: 0644]
components/tptp_grafite/.depend [new file with mode: 0644]
components/tptp_grafite/.depend.opt [new file with mode: 0644]
components/tptp_grafite/Makefile [new file with mode: 0644]
components/tptp_grafite/ast.ml [new file with mode: 0644]
components/tptp_grafite/heq_problems [new file with mode: 0644]
components/tptp_grafite/hne_problems [new file with mode: 0644]
components/tptp_grafite/lexer.mll [new file with mode: 0644]
components/tptp_grafite/main.ml [new file with mode: 0644]
components/tptp_grafite/parser.mly [new file with mode: 0644]
components/tptp_grafite/tptp2grafite.ml [new file with mode: 0644]
components/tptp_grafite/tptp2grafite.mli [new file with mode: 0644]
components/tptp_grafite/unit_equality_problems [new file with mode: 0644]
components/urimanager/.depend [new file with mode: 0644]
components/urimanager/.depend.opt [new file with mode: 0644]
components/urimanager/Makefile [new file with mode: 0644]
components/urimanager/uriManager.ml [new file with mode: 0644]
components/urimanager/uriManager.mli [new file with mode: 0644]
components/whelp/.depend [new file with mode: 0644]
components/whelp/.depend.opt [new file with mode: 0644]
components/whelp/Makefile [new file with mode: 0644]
components/whelp/fwdQueries.ml [new file with mode: 0644]
components/whelp/fwdQueries.mli [new file with mode: 0644]
components/whelp/whelp.ml [new file with mode: 0644]
components/whelp/whelp.mli [new file with mode: 0644]
components/xml/.depend [new file with mode: 0644]
components/xml/.depend.opt [new file with mode: 0644]
components/xml/Makefile [new file with mode: 0644]
components/xml/test.ml [new file with mode: 0644]
components/xml/xml.ml [new file with mode: 0644]
components/xml/xml.mli [new file with mode: 0644]
components/xml/xmlPushParser.ml [new file with mode: 0644]
components/xml/xmlPushParser.mli [new file with mode: 0644]
components/xmldiff/.depend [new file with mode: 0644]
components/xmldiff/.depend.opt [new file with mode: 0644]
components/xmldiff/Makefile [new file with mode: 0644]
components/xmldiff/xmlDiff.ml [new file with mode: 0644]
components/xmldiff/xmlDiff.mli [new file with mode: 0644]
configure.ac [new file with mode: 0644]
matita/.depend [new file with mode: 0644]
matita/.depend.opt [new file with mode: 0644]
matita/.ocamlinit [new file with mode: 0644]
matita/AUTHORS [new file with mode: 0644]
matita/LICENSE [new file with mode: 0644]
matita/Makefile [new file with mode: 0644]
matita/applyTransformation.ml [new file with mode: 0644]
matita/applyTransformation.mli [new file with mode: 0644]
matita/buildTimeConf.ml.in [new file with mode: 0644]
matita/closed.xml [new file with mode: 0644]
matita/contribs/CoRN-Decl/CoRN.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/Basics.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CAbGroups.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CFields.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CGroups.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CLogic.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CMonoids.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdAbs.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdFields.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/COrdFields2.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CPolynomials.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CRings.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSetoids.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CSums.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/Expon.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/algebra/ListType.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/AbsCC.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/CComplex.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/complex/NRootCC.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CC_Props.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/FTA.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/FTAreg.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/KeyLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/KneserLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/fta/MainLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Composition.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Continuity.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Derivative.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Differentiability.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FTC.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FunctSequence.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FunctSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/FunctSums.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Integral.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/NthDerivative.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/PartInterval.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Partitions.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefSepRef.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefSeparated.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/RefSeparating.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Rolle.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/StrongIVT.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/Taylor.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ftc/WeakIVT.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/makefile [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/ContFunctions.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/Equiv.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/fields/Qfield.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/Qgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/groups/Zgroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/rings/Qring.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/rings/Zring.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Npossec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Nsec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Qpossec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Qsec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/model/structures/Zsec.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/ordine_compilazione.txt [new file with mode: 0644]
matita/contribs/CoRN-Decl/preamble.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Bridges_iso.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CMetricFields.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CReals1.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CSumsReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/CauchySeq.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/IVT.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Intervals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/NRootIR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Q_dense.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/R_morphism.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/RealFuncts.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/RealLists.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/Series.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/reals/iso_CReals.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/AlgReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/FieldReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/GroupReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/RingReflection.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/Step.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/Exponential.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/InvTrigonom.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/Pi.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/PowerSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/RealPowers.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/SinCos.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/TaylorSeries.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/TrigMon.ma [new file with mode: 0644]
matita/contribs/CoRN-Decl/transc/Trigonometric.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/spare.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/theory.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/.depend [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/depends [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/theory.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/app/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sty0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sty0/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sty0/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sty1/cnt.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sty1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sty1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/sty0.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wf3/clear.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wf3/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wf3/fwd.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wf3/getl.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wf3/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wf3/ty3.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-1/coq/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-1/coq/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-1/definitions.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-1/preamble.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-1/spare.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-1/theory.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-2/.depend [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-2/depends [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Makefile [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/root [new file with mode: 0644]
matita/contribs/LOGIC/CLE/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/Insert/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/Insert/fun.ma [new file with mode: 0644]
matita/contribs/LOGIC/Insert/inv.ma [new file with mode: 0644]
matita/contribs/LOGIC/Insert/props.ma [new file with mode: 0644]
matita/contribs/LOGIC/Lift/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/Makefile [new file with mode: 0644]
matita/contribs/LOGIC/NTrack/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/NTrack/inv.ma [new file with mode: 0644]
matita/contribs/LOGIC/NTrack/order.ma [new file with mode: 0644]
matita/contribs/LOGIC/NTrack/props.ma [new file with mode: 0644]
matita/contribs/LOGIC/PEq/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/PNF/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/PRed/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/PRed/wlt.ma [new file with mode: 0644]
matita/contribs/LOGIC/Track/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/Track/inv.ma [new file with mode: 0644]
matita/contribs/LOGIC/Track/order.ma [new file with mode: 0644]
matita/contribs/LOGIC/Track/pred.ma [new file with mode: 0644]
matita/contribs/LOGIC/WLT/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/Weight/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/datatypes_defs/Context.ma [new file with mode: 0644]
matita/contribs/LOGIC/datatypes_defs/Formula.ma [new file with mode: 0644]
matita/contribs/LOGIC/datatypes_defs/Proof.ma [new file with mode: 0644]
matita/contribs/LOGIC/datatypes_defs/Sequent.ma [new file with mode: 0644]
matita/contribs/LOGIC/datatypes_props/Sequent.ma [new file with mode: 0644]
matita/contribs/LOGIC/depends [new file with mode: 0644]
matita/contribs/LOGIC/preamble0.ma [new file with mode: 0644]
matita/contribs/LOGIC/root [new file with mode: 0644]
matita/contribs/Makefile [new file with mode: 0644]
matita/contribs/Makefile.defs [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/defn.ma [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/defn2.ma [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/part1a.ma [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/part1a_inversion.ma [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/part1a_inversion2.ma [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/part1a_inversion3.ma [new file with mode: 0644]
matita/contribs/POPLmark/Fsub/util.ma [new file with mode: 0644]
matita/contribs/POPLmark/Makefile [new file with mode: 0644]
matita/contribs/POPLmark/depends [new file with mode: 0644]
matita/contribs/POPLmark/root [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/makefile [new file with mode: 0644]
matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/Makefile [new file with mode: 0644]
matita/contribs/RELATIONAL/NLE/defs.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NLE/inv.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NLE/nplus.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NLE/order.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NLE/props.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NPlus/defs.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NPlus/fun.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NPlus/inv.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NPlus/monoid.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NPlusList/defs.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NPlusList/props.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/ZEq/defs.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/ZEq/setoid.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/datatypes/Bool.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/datatypes/List.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/datatypes/Nat.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/datatypes/Zah.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/depends [new file with mode: 0644]
matita/contribs/RELATIONAL/preamble.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/root [new file with mode: 0644]
matita/contribs/assembly/Makefile [new file with mode: 0644]
matita/contribs/assembly/depends [new file with mode: 0644]
matita/contribs/assembly/freescale/aux_bases.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/byte8.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/doc/aurei.txt [new file with mode: 0644]
matita/contribs/assembly/freescale/doc/daa.txt [new file with mode: 0644]
matita/contribs/assembly/freescale/doc/freescale.txt [new file with mode: 0644]
matita/contribs/assembly/freescale/doc/ordinamento.txt [new file with mode: 0644]
matita/contribs/assembly/freescale/doc/ordine_compilazione.txt [new file with mode: 0644]
matita/contribs/assembly/freescale/doc/reverse.txt [new file with mode: 0644]
matita/contribs/assembly/freescale/exadecim.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/extra.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/fix-mkanystatus.sh [new file with mode: 0755]
matita/contribs/assembly/freescale/fix-with-left-params.diff [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/Makefile [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_datatypes_bool.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_datatypes_compare.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_datatypes_constructors.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_aux_bases.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_byte8.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_debug.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_exadecim.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_extra.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_load_write.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_medium_tests.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_medium_tests_lemmas.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_medium_tests_tools.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_abs.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_bits.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_func.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_struct.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_memory_trees.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_micro_tests.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_model.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_multivm.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_opcode.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_status.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_table_HC05.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_table_HC08.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_table_HCS08.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_table_RS08.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_higher_order_defs_functions.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_list_list.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_logic_connectives.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_logic_equality.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_compare.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_div_and_mod.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_exp.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_factorial.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_minimization.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_minus.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_nat.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_plus.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_primes.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_sigma_and_pi.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_times.ml [new file with mode: 0644]
matita/contribs/assembly/freescale/load_write.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/medium_tests.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/medium_tests_lemmas.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/medium_tests_tools.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/memory_abs.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/memory_bits.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/memory_func.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/memory_struct.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/memory_trees.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/micro_tests.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/model.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/multivm.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/opcode.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/status.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_HC05.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_HC05_tests.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_HC08.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_HC08_tests.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_HCS08.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_HCS08_tests.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_RS08.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/table_RS08_tests.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/tests.old [new file with mode: 0644]
matita/contribs/assembly/freescale/translation.ma [new file with mode: 0644]
matita/contribs/assembly/freescale/word16.ma [new file with mode: 0644]
matita/contribs/assembly/root [new file with mode: 0644]
matita/contribs/dama/Makefile [new file with mode: 0644]
matita/contribs/dama/dama/Makefile [new file with mode: 0644]
matita/contribs/dama/dama/Q_is_orded_divisble_group.ma [new file with mode: 0644]
matita/contribs/dama/dama/TODO [new file with mode: 0644]
matita/contribs/dama/dama/attic/fields.ma [new file with mode: 0644]
matita/contribs/dama/dama/attic/integration_algebras.ma [new file with mode: 0644]
matita/contribs/dama/dama/attic/ordered_fields_ch0.ma [new file with mode: 0644]
matita/contribs/dama/dama/attic/reals.ma [new file with mode: 0644]
matita/contribs/dama/dama/attic/rings.ma [new file with mode: 0644]
matita/contribs/dama/dama/attic/vector_spaces.ma [new file with mode: 0644]
matita/contribs/dama/dama/classical_pointfree/ordered_sets.ma [new file with mode: 0644]
matita/contribs/dama/dama/classical_pointfree/ordered_sets2.ma [new file with mode: 0644]
matita/contribs/dama/dama/classical_pointwise/sets.ma [new file with mode: 0644]
matita/contribs/dama/dama/classical_pointwise/sigma_algebra.ma [new file with mode: 0644]
matita/contribs/dama/dama/classical_pointwise/topology.ma [new file with mode: 0644]
matita/contribs/dama/dama/constructive_connectives.ma [new file with mode: 0644]
matita/contribs/dama/dama/constructive_higher_order_relations.ma [new file with mode: 0644]
matita/contribs/dama/dama/constructive_pointfree/lebesgue.ma [new file with mode: 0644]
matita/contribs/dama/dama/depends [new file with mode: 0644]
matita/contribs/dama/dama/divisible_group.ma [new file with mode: 0644]
matita/contribs/dama/dama/doc/DIMOSTRAZIONE [new file with mode: 0644]
matita/contribs/dama/dama/doc/NotaReticoli.pdf [new file with mode: 0644]
matita/contribs/dama/dama/excess.ma [new file with mode: 0644]
matita/contribs/dama/dama/group.ma [new file with mode: 0644]
matita/contribs/dama/dama/infsup.ma [new file with mode: 0644]
matita/contribs/dama/dama/lattice.ma [new file with mode: 0644]
matita/contribs/dama/dama/limit.ma [new file with mode: 0644]
matita/contribs/dama/dama/metric_lattice.ma [new file with mode: 0644]
matita/contribs/dama/dama/metric_space.ma [new file with mode: 0644]
matita/contribs/dama/dama/ordered_divisible_group.ma [new file with mode: 0644]
matita/contribs/dama/dama/ordered_group.ma [new file with mode: 0644]
matita/contribs/dama/dama/premetric_lattice.ma [new file with mode: 0644]
matita/contribs/dama/dama/prevalued_lattice.ma [new file with mode: 0644]
matita/contribs/dama/dama/root [new file with mode: 0644]
matita/contribs/dama/dama/sandwich.ma [new file with mode: 0644]
matita/contribs/dama/dama/sandwich_corollary.ma [new file with mode: 0644]
matita/contribs/dama/dama/sequence.ma [new file with mode: 0644]
matita/contribs/dama/dama/tend.ma [new file with mode: 0644]
matita/contribs/dama/dama_didactic/Makefile [new file with mode: 0644]
matita/contribs/dama/dama_didactic/bottom.ma [new file with mode: 0644]
matita/contribs/dama/dama_didactic/depends [new file with mode: 0644]
matita/contribs/dama/dama_didactic/deriv.ma [new file with mode: 0644]
matita/contribs/dama/dama_didactic/ex_deriv.ma [new file with mode: 0644]
matita/contribs/dama/dama_didactic/ex_seq.ma [new file with mode: 0644]
matita/contribs/dama/dama_didactic/reals.ma [new file with mode: 0644]
matita/contribs/dama/dama_didactic/root [new file with mode: 0644]
matita/contribs/dama/dama_didactic/sequences.ma [new file with mode: 0644]
matita/contribs/developments.txt [new file with mode: 0644]
matita/contribs/formal_topology/bin/Makefile [new file with mode: 0644]
matita/contribs/formal_topology/bin/formal_topology.ma [new file with mode: 0644]
matita/contribs/formal_topology/bin/theory_explorer.ml [new file with mode: 0644]
matita/contribs/formal_topology/bin/theory_explorer_do_not_trust_auto.ml [new file with mode: 0644]
matita/contribs/formal_topology/formal_topology.ma [new file with mode: 0644]
matita/contribs/formal_topology/formal_topology2.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/Q/q.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/Z/compare.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/Z/orders.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/Z/plus.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/Z/times.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/Z/z.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/chinese_reminder.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/compare.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/congruence.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/count.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/div_and_mod.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/euler_theorem.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/exp.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/factorial.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/factorization.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/fermat_little_theorem.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/gcd.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/le_arith.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/lt_arith.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/map_iter_p.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/minimization.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/minus.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/nat.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/nth_prime.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/ord.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/orders.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/permutation.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/plus.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/primes.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/relevant_equations.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/sigma_and_pi.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/times.ma [new file with mode: 0644]
matita/contribs/library_auto/auto/nat/totient.ma [new file with mode: 0644]
matita/contribs/library_auto/makefile [new file with mode: 0644]
matita/core_notation.moo [new file with mode: 0644]
matita/dictionary-matita.xml [new file with mode: 0644]
matita/dist/BUGS [new file with mode: 0644]
matita/dist/COPYING [new file with mode: 0644]
matita/dist/ChangeLog [new file with mode: 0644]
matita/dist/INSTALL [new file with mode: 0644]
matita/dist/Makefile [new file with mode: 0644]
matita/dist/README [new file with mode: 0644]
matita/dist/configure.ac.sed [new file with mode: 0644]
matita/dist/fill_db.sh [new file with mode: 0755]
matita/dist/static_link/Makefile [new file with mode: 0644]
matita/dist/static_link/static_link.ml [new file with mode: 0644]
matita/doc/primer.txt [new file with mode: 0644]
matita/dump_moo.ml [new file with mode: 0644]
matita/gtkmathview.matita.conf.xml.in [new file with mode: 0644]
matita/help/C/Makefile [new file with mode: 0644]
matita/help/C/TODO [new file with mode: 0644]
matita/help/C/declarative_tactics_quickref.xml [new file with mode: 0644]
matita/help/C/docbook.css [new file with mode: 0644]
matita/help/C/figures/database.dia [new file with mode: 0644]
matita/help/C/figures/database.png [new file with mode: 0644]
matita/help/C/legal.xml [new file with mode: 0644]
matita/help/C/matita.xml [new file with mode: 0644]
matita/help/C/sec_commands.xml [new file with mode: 0644]
matita/help/C/sec_declarative_tactics.xml [new file with mode: 0644]
matita/help/C/sec_gettingstarted.xml [new file with mode: 0644]
matita/help/C/sec_install.xml [new file with mode: 0644]
matita/help/C/sec_intro.xml [new file with mode: 0644]
matita/help/C/sec_license.xml [new file with mode: 0644]
matita/help/C/sec_tacticals.xml [new file with mode: 0644]
matita/help/C/sec_tactics.xml [new file with mode: 0644]
matita/help/C/sec_terms.xml [new file with mode: 0644]
matita/help/C/sec_usernotation.xml [new file with mode: 0644]
matita/help/C/tactic_quickref.xml [new file with mode: 0644]
matita/help/C/tactics_quickref.xml [new file with mode: 0644]
matita/help/C/version.txt.in [new file with mode: 0644]
matita/help/C/xhtml1-transitional.dtd [new file with mode: 0644]
matita/help/C/xsl/matita-fo.xsl [new file with mode: 0644]
matita/help/C/xsl/matita-tex.xsl [new file with mode: 0644]
matita/help/C/xsl/matita-xhtml.xsl [new file with mode: 0644]
matita/help/C/xsl/tactic_quickref.xsl [new file with mode: 0644]
matita/icons/matita-32.xpm [new file with mode: 0644]
matita/icons/matita-bulb-high.png [new file with mode: 0644]
matita/icons/matita-bulb-low.png [new file with mode: 0644]
matita/icons/matita-bulb-medium.png [new file with mode: 0644]
matita/icons/matita-folder.png [new file with mode: 0644]
matita/icons/matita-object.png [new file with mode: 0644]
matita/icons/matita-theory.png [new file with mode: 0644]
matita/icons/matita.png [new file with mode: 0644]
matita/icons/matita_medium.png [new file with mode: 0644]
matita/icons/matita_small.png [new file with mode: 0644]
matita/icons/matita_very_small.png [new file with mode: 0644]
matita/icons/meegg.png [new file with mode: 0644]
matita/icons/whelp.png [new file with mode: 0644]
matita/icons/whelp.svg [new file with mode: 0644]
matita/lablGraphviz.ml [new file with mode: 0644]
matita/lablGraphviz.mli [new file with mode: 0644]
matita/legacy/Makefile [new file with mode: 0644]
matita/legacy/coq.ma [new file with mode: 0644]
matita/legacy/depends [new file with mode: 0644]
matita/legacy/root [new file with mode: 0644]
matita/library/Makefile [new file with mode: 0644]
matita/library/Q/Qaxioms.ma [new file with mode: 0644]
matita/library/Q/q.ma [new file with mode: 0644]
matita/library/Z/compare.ma [new file with mode: 0644]
matita/library/Z/dirichlet_product.ma [new file with mode: 0644]
matita/library/Z/inversion.ma [new file with mode: 0644]
matita/library/Z/moebius.ma [new file with mode: 0644]
matita/library/Z/orders.ma [new file with mode: 0644]
matita/library/Z/plus.ma [new file with mode: 0644]
matita/library/Z/sigma_p.ma [new file with mode: 0644]
matita/library/Z/times.ma [new file with mode: 0644]
matita/library/Z/z.ma [new file with mode: 0644]
matita/library/algebra/CoRN/SemiGroups.ma [new file with mode: 0644]
matita/library/algebra/CoRN/SetoidFun.ma [new file with mode: 0644]
matita/library/algebra/CoRN/SetoidInc.ma [new file with mode: 0644]
matita/library/algebra/CoRN/Setoids.ma [new file with mode: 0644]
matita/library/algebra/finite_groups.ma [new file with mode: 0644]
matita/library/algebra/groups.ma [new file with mode: 0644]
matita/library/algebra/monoids.ma [new file with mode: 0644]
matita/library/algebra/semigroups.ma [new file with mode: 0644]
matita/library/datatypes/bool.ma [new file with mode: 0644]
matita/library/datatypes/compare.ma [new file with mode: 0644]
matita/library/datatypes/constructors.ma [new file with mode: 0644]
matita/library/decidable_kit/decidable.ma [new file with mode: 0644]
matita/library/decidable_kit/eqtype.ma [new file with mode: 0644]
matita/library/decidable_kit/fgraph.ma [new file with mode: 0644]
matita/library/decidable_kit/fintype.ma [new file with mode: 0644]
matita/library/decidable_kit/list_aux.ma [new file with mode: 0644]
matita/library/decidable_kit/streicher.ma [new file with mode: 0644]
matita/library/demo/power_derivative.ma [new file with mode: 0644]
matita/library/demo/propositional_sequent_calculus.ma [new file with mode: 0644]
matita/library/demo/realisability.ma [new file with mode: 0644]
matita/library/depends [new file with mode: 0644]
matita/library/higher_order_defs/functions.ma [new file with mode: 0644]
matita/library/higher_order_defs/ordering.ma [new file with mode: 0644]
matita/library/higher_order_defs/relations.ma [new file with mode: 0644]
matita/library/list/in.ma [new file with mode: 0644]
matita/library/list/list.ma [new file with mode: 0644]
matita/library/list/sort.ma [new file with mode: 0644]
matita/library/logic/coimplication.ma [new file with mode: 0644]
matita/library/logic/connectives.ma [new file with mode: 0644]
matita/library/logic/connectives2.ma [new file with mode: 0644]
matita/library/logic/equality.ma [new file with mode: 0644]
matita/library/nat/bertrand.ma [new file with mode: 0644]
matita/library/nat/binomial.ma [new file with mode: 0644]
matita/library/nat/chebyshev.ma [new file with mode: 0644]
matita/library/nat/chebyshev_teta.ma [new file with mode: 0644]
matita/library/nat/chebyshev_thm.ma [new file with mode: 0644]
matita/library/nat/chinese_reminder.ma [new file with mode: 0644]
matita/library/nat/compare.ma [new file with mode: 0644]
matita/library/nat/congruence.ma [new file with mode: 0644]
matita/library/nat/count.ma [new file with mode: 0644]
matita/library/nat/div_and_mod.ma [new file with mode: 0644]
matita/library/nat/div_and_mod_diseq.ma [new file with mode: 0644]
matita/library/nat/div_and_mod_new.ma.dontcompile [new file with mode: 0644]
matita/library/nat/euler_theorem.ma [new file with mode: 0644]
matita/library/nat/exp.ma [new file with mode: 0644]
matita/library/nat/factorial.ma [new file with mode: 0644]
matita/library/nat/factorial2.ma [new file with mode: 0644]
matita/library/nat/factorization.ma [new file with mode: 0644]
matita/library/nat/fermat_little_theorem.ma [new file with mode: 0644]
matita/library/nat/gcd.ma [new file with mode: 0644]
matita/library/nat/gcd_properties1.ma [new file with mode: 0644]
matita/library/nat/generic_iter_p.ma [new file with mode: 0644]
matita/library/nat/iteration2.ma [new file with mode: 0644]
matita/library/nat/le_arith.ma [new file with mode: 0644]
matita/library/nat/log.ma [new file with mode: 0644]
matita/library/nat/lt_arith.ma [new file with mode: 0644]
matita/library/nat/map_iter_p.ma [new file with mode: 0644]
matita/library/nat/minimization.ma [new file with mode: 0644]
matita/library/nat/minus.ma [new file with mode: 0644]
matita/library/nat/nat.ma [new file with mode: 0644]
matita/library/nat/neper.ma [new file with mode: 0644]
matita/library/nat/nth_prime.ma [new file with mode: 0644]
matita/library/nat/o.ma [new file with mode: 0644]
matita/library/nat/ord.ma [new file with mode: 0644]
matita/library/nat/orders.ma [new file with mode: 0644]
matita/library/nat/permutation.ma [new file with mode: 0644]
matita/library/nat/pi_p.ma [new file with mode: 0644]
matita/library/nat/plus.ma [new file with mode: 0644]
matita/library/nat/primes.ma [new file with mode: 0644]
matita/library/nat/relevant_equations.ma [new file with mode: 0644]
matita/library/nat/sigma_and_pi.ma [new file with mode: 0644]
matita/library/nat/sqrt.ma [new file with mode: 0644]
matita/library/nat/times.ma [new file with mode: 0644]
matita/library/nat/totient.ma [new file with mode: 0644]
matita/library/nat/totient1.ma [new file with mode: 0644]
matita/library/root [new file with mode: 0644]
matita/library/technicalities/setoids.ma [new file with mode: 0644]
matita/matita.conf.xml.in [new file with mode: 0644]
matita/matita.glade [new file with mode: 0644]
matita/matita.gtkrc [new file with mode: 0644]
matita/matita.lang [new file with mode: 0644]
matita/matita.ma.templ [new file with mode: 0644]
matita/matita.ml [new file with mode: 0644]
matita/matita.txt [new file with mode: 0644]
matita/matitaAutoGui.ml [new file with mode: 0644]
matita/matitaAutoGui.mli [new file with mode: 0644]
matita/matitaEngine.ml [new file with mode: 0644]
matita/matitaEngine.mli [new file with mode: 0644]
matita/matitaExcPp.ml [new file with mode: 0644]
matita/matitaExcPp.mli [new file with mode: 0644]
matita/matitaGtkMisc.ml [new file with mode: 0644]
matita/matitaGtkMisc.mli [new file with mode: 0644]
matita/matitaGui.ml [new file with mode: 0644]
matita/matitaGui.mli [new file with mode: 0644]
matita/matitaGuiTypes.mli [new file with mode: 0644]
matita/matitaInit.ml [new file with mode: 0644]
matita/matitaInit.mli [new file with mode: 0644]
matita/matitaMathView.ml [new file with mode: 0644]
matita/matitaMathView.mli [new file with mode: 0644]
matita/matitaMisc.ml [new file with mode: 0644]
matita/matitaMisc.mli [new file with mode: 0644]
matita/matitaScript.ml [new file with mode: 0644]
matita/matitaScript.mli [new file with mode: 0644]
matita/matitaTypes.ml [new file with mode: 0644]
matita/matitaTypes.mli [new file with mode: 0644]
matita/matitaWiki.ml [new file with mode: 0644]
matita/matitac.ml [new file with mode: 0644]
matita/matitacLib.ml [new file with mode: 0644]
matita/matitacLib.mli [new file with mode: 0644]
matita/matitaclean.ml [new file with mode: 0644]
matita/matitaclean.mli [new file with mode: 0644]
matita/matitadep.ml [new file with mode: 0644]
matita/matitadep.mli [new file with mode: 0644]
matita/scripts/README [new file with mode: 0644]
matita/scripts/bench.sql [new file with mode: 0644]
matita/scripts/clean_db.sh [new file with mode: 0755]
matita/scripts/crontab [new file with mode: 0644]
matita/scripts/crontab.sh [new file with mode: 0644]
matita/scripts/functions.lua [new file with mode: 0755]
matita/scripts/profile_svn.sh [new file with mode: 0755]
matita/scripts/public_html/bench.php [new file with mode: 0644]
matita/scripts/public_html/common.php [new file with mode: 0644]
matita/scripts/public_html/composequery.php [new file with mode: 0644]
matita/scripts/public_html/index.html [new file with mode: 0644]
matita/scripts/public_html/showquery.php [new file with mode: 0644]
matita/scripts/public_html/style.css [new file with mode: 0644]
matita/tests/Makefile [new file with mode: 0644]
matita/tests/TPTP/README [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO001-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO003-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO003-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO004-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO004-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO005-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO005-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO006-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO006-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO009-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO009-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO010-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO010-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO011-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO011-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO012-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO012-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO013-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO013-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO016-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO017-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO018-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO034-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO069-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO071-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/BOO075-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL004-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL007-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL008-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL010-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL012-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL013-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL014-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL015-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL016-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL017-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL018-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL021-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL022-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL024-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL025-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL045-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL048-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL050-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL058-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL058-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL060-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL060-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL061-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL061-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL062-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL062-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL063-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL063-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL063-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL063-5.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL063-6.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-5.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-6.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-7.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-8.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL064-9.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL083-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL084-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL085-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/COL086-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP001-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP001-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP010-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP011-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP012-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP022-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP023-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP115-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP116-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP117-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP118-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP136-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP137-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP139-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP141-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP142-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP143-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP144-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP145-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP146-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP149-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP150-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP151-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP152-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP153-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP154-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP155-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP156-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP157-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP158-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP159-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP160-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP161-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP162-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP163-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP168-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP168-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP173-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP174-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP176-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP176-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP182-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP182-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP182-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP182-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP186-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP186-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP188-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP188-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP189-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP189-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP192-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP206-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP454-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP455-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP456-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP457-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP458-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP459-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP460-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP463-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP467-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP481-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP484-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP485-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP486-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP487-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP488-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP490-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP491-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP492-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP493-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP494-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP495-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP496-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP497-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP498-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP509-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP510-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP511-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP512-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP513-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP514-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP515-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP516-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP517-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP518-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP520-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP541-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP542-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP543-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP544-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP545-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP546-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP547-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP548-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP549-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP550-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP551-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP552-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP556-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP558-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP560-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP561-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP562-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP564-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP565-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP566-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP567-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP568-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP569-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP570-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP572-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP573-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP574-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP576-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP577-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP578-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP580-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP581-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP582-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP583-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP584-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP586-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP588-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP590-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP592-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP595-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP596-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP597-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP598-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP599-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP600-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP602-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP603-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP604-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP605-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP606-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP608-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP612-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP613-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP614-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP615-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/GRP616-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT008-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT033-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT034-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT039-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT039-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT040-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LAT045-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL110-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL112-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL113-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL114-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL115-2.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL132-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL133-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL134-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL135-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL139-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL140-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL141-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL153-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL154-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL155-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL156-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL157-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL158-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL161-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LCL164-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LDA001-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/LDA007-3.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG007-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG008-4.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG011-5.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG023-6.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG023-7.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG024-6.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/RNG024-7.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/ROB002-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/ROB009-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/ROB010-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/ROB013-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/ROB030-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/Veloci/SYN083-1.p.ma [new file with mode: 0644]
matita/tests/TPTP/classify.sh [new file with mode: 0755]
matita/tests/TPTP/compare.ods [new file with mode: 0644]
matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt [new file with mode: 0644]
matita/tests/TPTP/elenco_CASC.txt [new file with mode: 0644]
matita/tests/TPTP/elenco_problemi_rating0_ancora_da_risolvere.txt [new file with mode: 0644]
matita/tests/TPTP/elenco_problemi_veloci_per_test.txt [new file with mode: 0644]
matita/tests/TPTP/elenco_unsatisfiable.txt [new file with mode: 0644]
matita/tests/TPTP/fetch_results_tptp.lua [new file with mode: 0755]
matita/tests/TPTP/hne_problems.txt [new file with mode: 0644]
matita/tests/TPTP/log.120.orsay.txt [new file with mode: 0644]
matita/tests/TPTP/log.300.19-6.txt [new file with mode: 0644]
matita/tests/TPTP/log.300.26-5.menvcorti [new file with mode: 0644]
matita/tests/TPTP/log.300.26-5.menvcorti.con_rating [new file with mode: 0644]
matita/tests/TPTP/log.300.27-6.fixprove.fixsimpl-infergoal [new file with mode: 0644]
matita/tests/TPTP/log.300.28-6.fixprove.fixsimpl-infergoal [new file with mode: 0644]
matita/tests/TPTP/log.300.29-5.CASC [new file with mode: 0644]
matita/tests/TPTP/log.300.29-6.fix-demodulationgoalwithcurr [new file with mode: 0644]
matita/tests/TPTP/log.300.30-6.fixdemodgoalinpassive [new file with mode: 0644]
matita/tests/TPTP/log.600.15-7.comedasvn_stampapesomassimoeqinprovanellog.txt [new file with mode: 0644]
matita/tests/TPTP/log.600.22-7.matitaprover.txt [new file with mode: 0644]
matita/tests/TPTP/log.600.30-6.weghtNOTlookingatgoalsymbols [new file with mode: 0644]
matita/tests/TPTP/log.600.30-6.weghtlookingatgoalsymbols.txt [new file with mode: 0644]
matita/tests/TPTP/maxweight.txt [new file with mode: 0644]
matita/tests/TPTP/merge_sorted_logs.awk [new file with mode: 0644]
matita/tests/TPTP/prova_LAT145_rating_93.tar.gz [new file with mode: 0644]
matita/tests/TPTP/risultati_CASC_2005.txt [new file with mode: 0644]
matita/tests/TPTP/simulate_casc.sh [new file with mode: 0755]
matita/tests/TPTP/try.sh [new file with mode: 0755]
matita/tests/TPTP/unit_equality_problems.txt [new file with mode: 0644]
matita/tests/absurd.ma [new file with mode: 0644]
matita/tests/apply.ma [new file with mode: 0644]
matita/tests/apply2.ma [new file with mode: 0644]
matita/tests/applys.ma [new file with mode: 0644]
matita/tests/assumption.ma [new file with mode: 0644]
matita/tests/bad_induction.ma [new file with mode: 0644]
matita/tests/bad_tests/Makefile [new file with mode: 0644]
matita/tests/bad_tests/auto.log [new file with mode: 0644]
matita/tests/bad_tests/auto.ma [new file with mode: 0755]
matita/tests/bad_tests/baseuri.log [new file with mode: 0644]
matita/tests/bad_tests/baseuri.ma [new file with mode: 0644]
matita/tests/bool.ma [new file with mode: 0644]
matita/tests/change.ma [new file with mode: 0644]
matita/tests/clear.ma [new file with mode: 0644]
matita/tests/clearbody.ma [new file with mode: 0644]
matita/tests/coercions.ma [new file with mode: 0644]
matita/tests/coercions_contravariant.ma [new file with mode: 0644]
matita/tests/coercions_dependent.ma [new file with mode: 0644]
matita/tests/coercions_nonuniform.ma [new file with mode: 0644]
matita/tests/coercions_open.ma [new file with mode: 0644]
matita/tests/coercions_propagation.ma [new file with mode: 0644]
matita/tests/coercions_russell.ma [new file with mode: 0644]
matita/tests/comments.ma [new file with mode: 0644]
matita/tests/compose.ma [new file with mode: 0644]
matita/tests/constructor.ma [new file with mode: 0644]
matita/tests/continuationals.ma [new file with mode: 0644]
matita/tests/contradiction.ma [new file with mode: 0644]
matita/tests/cut.ma [new file with mode: 0644]
matita/tests/decl.ma [new file with mode: 0644]
matita/tests/decompose.ma [new file with mode: 0644]
matita/tests/demodulation_coq.ma [new file with mode: 0644]
matita/tests/demodulation_matita.ma [new file with mode: 0644]
matita/tests/dependent_guarded_bove_capretta.ma [new file with mode: 0644]
matita/tests/dependent_injection.ma [new file with mode: 0644]
matita/tests/dependent_type_inference.ma [new file with mode: 0644]
matita/tests/depends [new file with mode: 0644]
matita/tests/destruct.ma [new file with mode: 0644]
matita/tests/elim.ma [new file with mode: 0644]
matita/tests/fguidi.ma [new file with mode: 0644]
matita/tests/first.ma [new file with mode: 0644]
matita/tests/fix_betareduction.ma [new file with mode: 0644]
matita/tests/fix_che_non_passa_ma_dovrebbe.ma [new file with mode: 0644]
matita/tests/fold.ma [new file with mode: 0644]
matita/tests/generalize.ma [new file with mode: 0644]
matita/tests/hard_refine.ma [new file with mode: 0644]
matita/tests/injection.ma [new file with mode: 0644]
matita/tests/interactive/automatic_insertion.ma [new file with mode: 0644]
matita/tests/interactive/drop.ma [new file with mode: 0644]
matita/tests/interactive/grafite.ma [new file with mode: 0644]
matita/tests/interactive/test5.ma [new file with mode: 0644]
matita/tests/interactive/test6.ma [new file with mode: 0644]
matita/tests/interactive/test7.ma [new file with mode: 0644]
matita/tests/interactive/test_instance.ma [new file with mode: 0644]
matita/tests/inversion.ma [new file with mode: 0644]
matita/tests/inversion2.ma [new file with mode: 0644]
matita/tests/letrec.ma [new file with mode: 0644]
matita/tests/letrecand.ma [new file with mode: 0644]
matita/tests/match_inference.ma [new file with mode: 0644]
matita/tests/metasenv_ordering.ma [new file with mode: 0644]
matita/tests/multiple_inheritance.ma [new file with mode: 0644]
matita/tests/mysql_escaping.ma [new file with mode: 0644]
matita/tests/naiveparamod.ma [new file with mode: 0644]
matita/tests/overred.ma [new file with mode: 0644]
matita/tests/paramodulation.ma [new file with mode: 0644]
matita/tests/paramodulation/BOO075-1.ma [new file with mode: 0644]
matita/tests/paramodulation/boolean_algebra.ma [new file with mode: 0644]
matita/tests/paramodulation/group.ma [new file with mode: 0644]
matita/tests/paramodulation/irratsqrt2.ma [new file with mode: 0644]
matita/tests/pullback.ma [new file with mode: 0644]
matita/tests/record.ma [new file with mode: 0644]
matita/tests/replace.ma [new file with mode: 0644]
matita/tests/rewrite.ma [new file with mode: 0644]
matita/tests/root [new file with mode: 0644]
matita/tests/second.ma [new file with mode: 0644]
matita/tests/simpl.ma [new file with mode: 0644]
matita/tests/tacticals.ma [new file with mode: 0644]
matita/tests/test2.ma [new file with mode: 0644]
matita/tests/test3.ma [new file with mode: 0644]
matita/tests/test4.ma [new file with mode: 0644]
matita/tests/third.ma [new file with mode: 0644]
matita/tests/tinycals.ma [new file with mode: 0644]
matita/tests/unfold.ma [new file with mode: 0644]