git://colo12-c703.uibk.ac.at / hl193./.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(initial) | patch
Update from HH master
authorCezary Kaliszyk <cek@colo12-c703.uibk.ac.at>
Tue, 26 Aug 2014 13:04:35 +0000 (15:04 +0200)
committerCezary Kaliszyk <cek@colo12-c703.uibk.ac.at>
Tue, 26 Aug 2014 13:04:35 +0000 (15:04 +0200)
commitd6b1195ce8ec9090113ae31a1dcece4bac145872
treeb997f9ba08d1573f70ec2902fc308a8e6ec1051ctree | snapshot
Update from HH
414 files changed:
100/arithmetic.ml [new file with mode: 0644] blob
100/arithmetic_geometric_mean.ml [new file with mode: 0644] blob
100/ballot.ml [new file with mode: 0644] blob
100/bernoulli.ml [new file with mode: 0644] blob
100/bertrand.ml [new file with mode: 0644] blob
100/birthday.ml [new file with mode: 0644] blob
100/cantor.ml [new file with mode: 0644] blob
100/cayley_hamilton.ml [new file with mode: 0644] blob
100/ceva.ml [new file with mode: 0644] blob
100/chords.ml [new file with mode: 0644] blob
100/circle.ml [new file with mode: 0644] blob
100/combinations.ml [new file with mode: 0644] blob
100/constructible.ml [new file with mode: 0644] blob
100/cosine.ml [new file with mode: 0644] blob
100/cubic.ml [new file with mode: 0644] blob
100/derangements.ml [new file with mode: 0644] blob
100/desargues.ml [new file with mode: 0644] blob
100/descartes.ml [new file with mode: 0644] blob
100/dirichlet.ml [new file with mode: 0644] blob
100/div3.ml [new file with mode: 0644] blob
100/divharmonic.ml [new file with mode: 0644] blob
100/e_is_transcendental.ml [new file with mode: 0644] blob
100/euler.ml [new file with mode: 0644] blob
100/feuerbach.ml [new file with mode: 0644] blob
100/four_squares.ml [new file with mode: 0644] blob
100/fourier.ml [new file with mode: 0644] blob
100/friendship.ml [new file with mode: 0644] blob
100/fta.ml [new file with mode: 0644] blob
100/gcd.ml [new file with mode: 0644] blob
100/heron.ml [new file with mode: 0644] blob
100/inclusion_exclusion.ml [new file with mode: 0644] blob
100/independence.ml [new file with mode: 0644] blob
100/isosceles.ml [new file with mode: 0644] blob
100/konigsberg.ml [new file with mode: 0644] blob
100/lagrange.ml [new file with mode: 0644] blob
100/leibniz.ml [new file with mode: 0644] blob
100/lhopital.ml [new file with mode: 0644] blob
100/liouville.ml [new file with mode: 0644] blob
100/minkowski.ml [new file with mode: 0644] blob
100/morley.ml [new file with mode: 0644] blob
100/pascal.ml [new file with mode: 0644] blob
100/perfect.ml [new file with mode: 0644] blob
100/pick.ml [new file with mode: 0644] blob
100/piseries.ml [new file with mode: 0644] blob
100/platonic.ml [new file with mode: 0644] blob
100/pnt.ml [new file with mode: 0644] blob
100/polyhedron.ml [new file with mode: 0644] blob
100/primerecip.ml [new file with mode: 0644] blob
100/ptolemy.ml [new file with mode: 0644] blob
100/pythagoras.ml [new file with mode: 0644] blob
100/quartic.ml [new file with mode: 0644] blob
100/ramsey.ml [new file with mode: 0644] blob
100/ratcountable.ml [new file with mode: 0644] blob
100/realsuncountable.ml [new file with mode: 0644] blob
100/reciprocity.ml [new file with mode: 0644] blob
100/sqrt.ml [new file with mode: 0644] blob
100/stirling.ml [new file with mode: 0644] blob
100/subsequence.ml [new file with mode: 0644] blob
100/thales.ml [new file with mode: 0644] blob
100/triangular.ml [new file with mode: 0644] blob
100/two_squares.ml [new file with mode: 0644] blob
100/wilson.ml [new file with mode: 0644] blob
Arithmetic/arithprov.ml [new file with mode: 0644] blob
Arithmetic/definability.ml [new file with mode: 0644] blob
Arithmetic/derived.ml [new file with mode: 0644] blob
Arithmetic/fol.ml [new file with mode: 0644] blob
Arithmetic/godel.ml [new file with mode: 0644] blob
Arithmetic/make.ml [new file with mode: 0644] blob
Arithmetic/pa.ml [new file with mode: 0644] blob
Arithmetic/sigmacomplete.ml [new file with mode: 0644] blob
Arithmetic/tarski.ml [new file with mode: 0644] blob
Boyer_Moore/boyer-moore.ml [new file with mode: 0644] blob
Boyer_Moore/clausal_form.ml [new file with mode: 0644] blob
Boyer_Moore/counterexample.ml [new file with mode: 0644] blob
Boyer_Moore/definitions.ml [new file with mode: 0644] blob
Boyer_Moore/environment.ml [new file with mode: 0644] blob
Boyer_Moore/equalities.ml [new file with mode: 0644] blob
Boyer_Moore/generalize.ml [new file with mode: 0644] blob
Boyer_Moore/induction.ml [new file with mode: 0644] blob
Boyer_Moore/irrelevance.ml [new file with mode: 0644] blob
Boyer_Moore/main.ml [new file with mode: 0644] blob
Boyer_Moore/make.ml [new file with mode: 0644] blob
Boyer_Moore/rewrite_rules.ml [new file with mode: 0644] blob
Boyer_Moore/shells.ml [new file with mode: 0644] blob
Boyer_Moore/struct_equal.ml [new file with mode: 0644] blob
Boyer_Moore/support.ml [new file with mode: 0644] blob
Boyer_Moore/terms_and_clauses.ml [new file with mode: 0644] blob
Boyer_Moore/testset/arith.ml [new file with mode: 0644] blob
Boyer_Moore/testset/list.ml [new file with mode: 0644] blob
Boyer_Moore/waterfall.ml [new file with mode: 0644] blob
Complex/complex_grobner.ml [new file with mode: 0644] blob
Complex/complex_real.ml [new file with mode: 0644] blob
Complex/complex_transc.ml [new file with mode: 0644] blob
Complex/complexnumbers.ml [new file with mode: 0644] blob
Complex/cpoly.ml [new file with mode: 0644] blob
Complex/fundamental.ml [new file with mode: 0644] blob
Complex/grobner_examples.ml [new file with mode: 0644] blob
Complex/make.ml [new file with mode: 0644] blob
Complex/quelim.ml [new file with mode: 0644] blob
Complex/quelim_examples.ml [new file with mode: 0644] blob
Examples/borsuk.ml [new file with mode: 0644] blob
Examples/brunn_minkowski.ml [new file with mode: 0644] blob
Examples/combin.ml [new file with mode: 0644] blob
Examples/cong.ml [new file with mode: 0644] blob
Examples/cooper.ml [new file with mode: 0644] blob
Examples/dickson.ml [new file with mode: 0644] blob
Examples/dlo.ml [new file with mode: 0644] blob
Examples/forster.ml [new file with mode: 0644] blob
Examples/gcdrecurrence.ml [new file with mode: 0644] blob
Examples/harmonicsum.ml [new file with mode: 0644] blob
Examples/hol88.ml [new file with mode: 0644] blob
Examples/holby.ml [new file with mode: 0644] blob
Examples/inverse_bug_puzzle_miz3.ml [new file with mode: 0644] blob
Examples/inverse_bug_puzzle_tac.ml [new file with mode: 0644] blob
Examples/kb.ml [new file with mode: 0644] blob
Examples/lagrange_lemma.ml [new file with mode: 0644] blob
Examples/lucas_lehmer.ml [new file with mode: 0644] blob
Examples/machin.ml [new file with mode: 0644] blob
Examples/mangoldt.ml [new file with mode: 0644] blob
Examples/mccarthy.ml [new file with mode: 0644] blob
Examples/mizar.ml [new file with mode: 0644] blob
Examples/multiwf.ml [new file with mode: 0644] blob
Examples/pell.ml [new file with mode: 0644] blob
Examples/polylog.ml [new file with mode: 0644] blob
Examples/prog.ml [new file with mode: 0644] blob
Examples/prover9.ml [new file with mode: 0644] blob
Examples/rectypes.ml [new file with mode: 0644] blob
Examples/reduct.ml [new file with mode: 0644] blob
Examples/schnirelmann.ml [new file with mode: 0644] blob
Examples/solovay.ml [new file with mode: 0644] blob
Examples/sos.ml [new file with mode: 0644] blob
Examples/ste.ml [new file with mode: 0644] blob
Examples/sylvester_gallai.ml [new file with mode: 0644] blob
Examples/update_database.ml [new file with mode: 0644] blob
Examples/vitali.ml [new file with mode: 0644] blob
IsabelleLight/isalight.ml [new file with mode: 0644] blob
IsabelleLight/make.ml [new file with mode: 0644] blob
IsabelleLight/meta_rules.ml [new file with mode: 0644] blob
IsabelleLight/new_tactics.ml [new file with mode: 0644] blob
IsabelleLight/support.ml [new file with mode: 0644] blob
Jordan/float.ml [new file with mode: 0644] blob
Jordan/jordan_curve_theorem.ml [new file with mode: 0644] blob
Jordan/lib_ext.ml [new file with mode: 0644] blob
Jordan/make.ml [new file with mode: 0644] blob
Jordan/metric_spaces.ml [new file with mode: 0644] blob
Jordan/misc_defs_and_lemmas.ml [new file with mode: 0644] blob
Jordan/num_ext_gcd.ml [new file with mode: 0644] blob
Jordan/num_ext_nabs.ml [new file with mode: 0644] blob
Jordan/parse_ext_override_interface.ml [new file with mode: 0644] blob
Jordan/real_ext.ml [new file with mode: 0644] blob
Jordan/real_ext_geom_series.ml [new file with mode: 0644] blob
Jordan/tactics_ext.ml [new file with mode: 0644] blob
Jordan/tactics_ext2.ml [new file with mode: 0644] blob
Jordan/tactics_fix.ml [new file with mode: 0644] blob
Jordan/tactics_refine.ml [new file with mode: 0644] blob
LP_arith/lp_arith.ml [new file with mode: 0644] blob
LP_arith/lp_tests.ml [new file with mode: 0644] blob
LP_arith/make.ml [new file with mode: 0644] blob
Library/agm.ml [new file with mode: 0644] blob
Library/analysis.ml [new file with mode: 0644] blob
Library/binary.ml [new file with mode: 0644] blob
Library/binomial.ml [new file with mode: 0644] blob
Library/calc_real.ml [new file with mode: 0644] blob
Library/card.ml [new file with mode: 0644] blob
Library/floor.ml [new file with mode: 0644] blob
Library/integer.ml [new file with mode: 0644] blob
Library/isum.ml [new file with mode: 0644] blob
Library/iter.ml [new file with mode: 0644] blob
Library/multiplicative.ml [new file with mode: 0644] blob
Library/permutations.ml [new file with mode: 0644] blob
Library/pocklington.ml [new file with mode: 0644] blob
Library/poly.ml [new file with mode: 0644] blob
Library/pratt.ml [new file with mode: 0644] blob
Library/prime.ml [new file with mode: 0644] blob
Library/primitive.ml [new file with mode: 0644] blob
Library/products.ml [new file with mode: 0644] blob
Library/rstc.ml [new file with mode: 0644] blob
Library/transc.ml [new file with mode: 0644] blob
Library/wo.ml [new file with mode: 0644] blob
Minisat/dimacs_tools.ml [new file with mode: 0644] blob
Minisat/make.ml [new file with mode: 0644] blob
Minisat/minisat_parse.ml [new file with mode: 0644] blob
Minisat/minisat_prove.ml [new file with mode: 0644] blob
Minisat/minisat_resolve.ml [new file with mode: 0644] blob
Minisat/sat_common_tools.ml [new file with mode: 0644] blob
Minisat/sat_script.ml [new file with mode: 0644] blob
Minisat/sat_solvers.ml [new file with mode: 0644] blob
Minisat/sat_tools.ml [new file with mode: 0644] blob
Minisat/taut.ml [new file with mode: 0644] blob
Mizarlight/duality.ml [new file with mode: 0644] blob
Mizarlight/duality_holby.ml [new file with mode: 0644] blob
Mizarlight/make.ml [new file with mode: 0644] blob
Mizarlight/miz2a.ml [new file with mode: 0644] blob
Mizarlight/pa_f.ml [new file with mode: 0644] blob
Model/make.ml [new file with mode: 0644] blob
Model/modelset.ml [new file with mode: 0644] blob
Model/semantics.ml [new file with mode: 0644] blob
Model/syntax.ml [new file with mode: 0644] blob
Multivariate/canal.ml [new file with mode: 0644] blob
Multivariate/cauchy.ml [new file with mode: 0644] blob
Multivariate/clifford.ml [new file with mode: 0644] blob
Multivariate/complex_database.ml [new file with mode: 0644] blob
Multivariate/complexes.ml [new file with mode: 0644] blob
Multivariate/convex.ml [new file with mode: 0644] blob
Multivariate/cross.ml [new file with mode: 0644] blob
Multivariate/derivatives.ml [new file with mode: 0644] blob
Multivariate/determinants.ml [new file with mode: 0644] blob
Multivariate/dimension.ml [new file with mode: 0644] blob
Multivariate/flyspeck.ml [new file with mode: 0644] blob
Multivariate/gamma.ml [new file with mode: 0644] blob
Multivariate/geom.ml [new file with mode: 0644] blob
Multivariate/integration.ml [new file with mode: 0644] blob
Multivariate/make.ml [new file with mode: 0644] blob
Multivariate/make_complex.ml [new file with mode: 0644] blob
Multivariate/measure.ml [new file with mode: 0644] blob
Multivariate/misc.ml [new file with mode: 0644] blob
Multivariate/moretop.ml [new file with mode: 0644] blob
Multivariate/multivariate_database.ml [new file with mode: 0644] blob
Multivariate/paths.ml [new file with mode: 0644] blob
Multivariate/polytope.ml [new file with mode: 0644] blob
Multivariate/realanalysis.ml [new file with mode: 0644] blob
Multivariate/tarski.ml [new file with mode: 0644] blob
Multivariate/topology.ml [new file with mode: 0644] blob
Multivariate/transcendentals.ml [new file with mode: 0644] blob
Multivariate/vectors.ml [new file with mode: 0644] blob
Multivariate/wlog.ml [new file with mode: 0644] blob
Multivariate/wlog_examples.ml [new file with mode: 0644] blob
Ntrie/ntrie.ml [new file with mode: 0644] blob
Ntrie/ntrie_tests.ml [new file with mode: 0644] blob
Permutation/make.ml [new file with mode: 0644] blob
Permutation/morelist.ml [new file with mode: 0644] blob
Permutation/nummax.ml [new file with mode: 0644] blob
Permutation/permutation.ml [new file with mode: 0644] blob
Permutation/permuted.ml [new file with mode: 0644] blob
Permutation/qsort.ml [new file with mode: 0644] blob
Proofrecording/diffs/basics.ml [new file with mode: 0644] blob
Proofrecording/diffs/bool.ml [new file with mode: 0644] blob
Proofrecording/diffs/depgraph.ml [new file with mode: 0644] blob
Proofrecording/diffs/equal.ml [new file with mode: 0644] blob
Proofrecording/diffs/hol.ml [new file with mode: 0644] blob
Proofrecording/diffs/proofobjects_coq.ml [new file with mode: 0644] blob
Proofrecording/diffs/proofobjects_dummy.ml [new file with mode: 0644] blob
Proofrecording/diffs/proofobjects_init.ml [new file with mode: 0644] blob
Proofrecording/diffs/proofobjects_trt.ml [new file with mode: 0644] blob
Proofrecording/diffs/tactics.ml [new file with mode: 0644] blob
Proofrecording/diffs/thm.ml [new file with mode: 0644] blob
Proofrecording/tools/init.ml [new file with mode: 0644] blob
Proofrecording/tools/startcore.ml [new file with mode: 0644] blob
QBF/make.ml [new file with mode: 0644] blob
QBF/mygraph.ml [new file with mode: 0644] blob
QBF/qbf.ml [new file with mode: 0644] blob
QBF/qbfr.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/HilbertAxiom_read.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/Topology.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/UniversalPropCartProd.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/error-checking.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/from_topology.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/inverse_bug_puzzle_read.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/miz3/FontHilbertAxiom.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/miz3/HilbertAxiom.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/miz3/make.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/readable.ml [new file with mode: 0644] blob
RichterHilbertAxiomGeometry/thmFontHilbertAxiom.ml [new file with mode: 0644] blob
Rqe/asym.ml [new file with mode: 0644] blob
Rqe/basic.ml [new file with mode: 0644] blob
Rqe/condense.ml [new file with mode: 0644] blob
Rqe/condense_thms.ml [new file with mode: 0644] blob
Rqe/dedmatrix.ml [new file with mode: 0644] blob
Rqe/dedmatrix_thms.ml [new file with mode: 0644] blob
Rqe/defs.ml [new file with mode: 0644] blob
Rqe/examples.ml [new file with mode: 0644] blob
Rqe/inferisign.ml [new file with mode: 0644] blob
Rqe/inferisign_thms.ml [new file with mode: 0644] blob
Rqe/inferpsign.ml [new file with mode: 0644] blob
Rqe/inferpsign_thms.ml [new file with mode: 0644] blob
Rqe/lift_qelim.ml [new file with mode: 0644] blob
Rqe/list_rewrites.ml [new file with mode: 0644] blob
Rqe/main_thms.ml [new file with mode: 0644] blob
Rqe/make.ml [new file with mode: 0644] blob
Rqe/matinsert.ml [new file with mode: 0644] blob
Rqe/matinsert_thms.ml [new file with mode: 0644] blob
Rqe/num_calc_simp.ml [new file with mode: 0644] blob
Rqe/pdivides.ml [new file with mode: 0644] blob
Rqe/pdivides_thms.ml [new file with mode: 0644] blob
Rqe/poly_ext.ml [new file with mode: 0644] blob
Rqe/rewrites.ml [new file with mode: 0644] blob
Rqe/rol.ml [new file with mode: 0644] blob
Rqe/rqe_lib.ml [new file with mode: 0644] blob
Rqe/rqe_list.ml [new file with mode: 0644] blob
Rqe/rqe_main.ml [new file with mode: 0644] blob
Rqe/rqe_num.ml [new file with mode: 0644] blob
Rqe/rqe_real.ml [new file with mode: 0644] blob
Rqe/rqe_tactics_ext.ml [new file with mode: 0644] blob
Rqe/signs.ml [new file with mode: 0644] blob
Rqe/signs_thms.ml [new file with mode: 0644] blob
Rqe/simplify.ml [new file with mode: 0644] blob
Rqe/testform.ml [new file with mode: 0644] blob
Rqe/testform_thms.ml [new file with mode: 0644] blob
Rqe/timers.ml [new file with mode: 0644] blob
Rqe/util.ml [new file with mode: 0644] blob
Rqe/work_thms.ml [new file with mode: 0644] blob
Tutorial/Abstractions_and_quantifiers.ml [new file with mode: 0644] blob
Tutorial/Changing_proof_style.ml [new file with mode: 0644] blob
Tutorial/Custom_inference_rules.ml [new file with mode: 0644] blob
Tutorial/Custom_tactics.ml [new file with mode: 0644] blob
Tutorial/Defining_new_types.ml [new file with mode: 0644] blob
Tutorial/Embedding_of_logics_deep.ml [new file with mode: 0644] blob
Tutorial/Embedding_of_logics_shallow.ml [new file with mode: 0644] blob
Tutorial/HOL_as_a_functional_programming_language.ml [new file with mode: 0644] blob
Tutorial/HOL_basics.ml [new file with mode: 0644] blob
Tutorial/HOLs_number_systems.ml [new file with mode: 0644] blob
Tutorial/Inductive_datatypes.ml [new file with mode: 0644] blob
Tutorial/Inductive_definitions.ml [new file with mode: 0644] blob
Tutorial/Linking_external_tools.ml [new file with mode: 0644] blob
Tutorial/Number_theory.ml [new file with mode: 0644] blob
Tutorial/Propositional_logic.ml [new file with mode: 0644] blob
Tutorial/Real_analysis.ml [new file with mode: 0644] blob
Tutorial/Recursive_definitions.ml [new file with mode: 0644] blob
Tutorial/Semantics_of_programming_languages_deep.ml [new file with mode: 0644] blob
Tutorial/Semantics_of_programming_languages_shallow.ml [new file with mode: 0644] blob
Tutorial/Sets_and_functions.ml [new file with mode: 0644] blob
Tutorial/Tactics_and_tacticals.ml [new file with mode: 0644] blob
Tutorial/Vectors.ml [new file with mode: 0644] blob
Tutorial/Wellfounded_induction.ml [new file with mode: 0644] blob
Tutorial/all.ml [new file with mode: 0644] blob
Unity/aux_definitions.ml [new file with mode: 0644] blob
Unity/make.ml [new file with mode: 0644] blob
Unity/mk_comp_unity.ml [new file with mode: 0644] blob
Unity/mk_ensures.ml [new file with mode: 0644] blob
Unity/mk_gen_induct.ml [new file with mode: 0644] blob
Unity/mk_leadsto.ml [new file with mode: 0644] blob
Unity/mk_state_logic.ml [new file with mode: 0644] blob
Unity/mk_unity_prog.ml [new file with mode: 0644] blob
Unity/mk_unless.ml [new file with mode: 0644] blob
arith.ml [new file with mode: 0644] blob
basics.ml [new file with mode: 0644] blob
bool.ml [new file with mode: 0644] blob
calc_int.ml [new file with mode: 0644] blob
calc_num.ml [new file with mode: 0644] blob
calc_rat.ml [new file with mode: 0644] blob
canon.ml [new file with mode: 0644] blob
cart.ml [new file with mode: 0644] blob
class.ml [new file with mode: 0644] blob
database.ml [new file with mode: 0644] blob
define.ml [new file with mode: 0644] blob
drule.ml [new file with mode: 0644] blob
equal.ml [new file with mode: 0644] blob
grobner.ml [new file with mode: 0644] blob
help.ml [new file with mode: 0644] blob
hol.ml [new file with mode: 0644] blob
impconv.ml [new file with mode: 0644] blob
ind_defs.ml [new file with mode: 0644] blob
ind_types.ml [new file with mode: 0644] blob
int.ml [new file with mode: 0644] blob
itab.ml [new file with mode: 0644] blob
iterate.ml [new file with mode: 0644] blob
lib.ml [new file with mode: 0644] blob
lists.ml [new file with mode: 0644] blob
make.ml [new file with mode: 0644] blob
meson.ml [new file with mode: 0644] blob
miz3/Samples/bug0.ml [new file with mode: 0644] blob
miz3/Samples/bug1.ml [new file with mode: 0644] blob
miz3/Samples/bug2.ml [new file with mode: 0644] blob
miz3/Samples/bug3.ml [new file with mode: 0644] blob
miz3/Samples/drinker.ml [new file with mode: 0644] blob
miz3/Samples/forster.ml [new file with mode: 0644] blob
miz3/Samples/icms.ml [new file with mode: 0644] blob
miz3/Samples/irrat2.ml [new file with mode: 0644] blob
miz3/Samples/lagrange.ml [new file with mode: 0644] blob
miz3/Samples/lagrange1.ml [new file with mode: 0644] blob
miz3/Samples/luxury.ml [new file with mode: 0644] blob
miz3/Samples/other_mizs.ml [new file with mode: 0644] blob
miz3/Samples/robbins.ml [new file with mode: 0644] blob
miz3/Samples/sample.ml [new file with mode: 0644] blob
miz3/Samples/samples.ml [new file with mode: 0644] blob
miz3/Samples/talk.ml [new file with mode: 0644] blob
miz3/Samples/tobias.ml [new file with mode: 0644] blob
miz3/Samples/wishes.ml [new file with mode: 0644] blob
miz3/make.ml [new file with mode: 0644] blob
miz3/miz3.ml [new file with mode: 0644] blob
miz3/miz3_of_hol.ml [new file with mode: 0644] blob
miz3/test.ml [new file with mode: 0644] blob
nets.ml [new file with mode: 0644] blob
normalizer.ml [new file with mode: 0644] blob
nums.ml [new file with mode: 0644] blob
pa_j.ml [new file with mode: 0644] blob
pa_j_3.07.ml [new file with mode: 0644] blob
pa_j_3.08.ml [new file with mode: 0644] blob
pa_j_3.09.ml [new file with mode: 0644] blob
pa_j_3.1x_5.xx.ml [new file with mode: 0644] blob
pa_j_3.1x_6.02.1.ml [new file with mode: 0644] blob
pa_j_3.1x_6.02.2.ml [new file with mode: 0644] blob
pa_j_3.1x_6.11.ml [new file with mode: 0644] blob
pa_j_3.1x_6.xx.ml [new file with mode: 0644] blob
pair.ml [new file with mode: 0644] blob
parser.ml [new file with mode: 0644] blob
preterm.ml [new file with mode: 0644] blob
printer.ml [new file with mode: 0644] blob
quot.ml [new file with mode: 0644] blob
real.ml [new file with mode: 0644] blob
realarith.ml [new file with mode: 0644] blob
realax.ml [new file with mode: 0644] blob
recursion.ml [new file with mode: 0644] blob
sets.ml [new file with mode: 0644] blob
simp.ml [new file with mode: 0644] blob
system.ml [new file with mode: 0644] blob
tactics.ml [new file with mode: 0644] blob
term.ml [new file with mode: 0644] blob
theorems.ml [new file with mode: 0644] blob
thm.ml [new file with mode: 0644] blob
trivia.ml [new file with mode: 0644] blob
type.ml [new file with mode: 0644] blob
update_database.ml [new file with mode: 0644] blob
wf.ml [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.