git://colo12-c703.uibk.ac.at / Flyspeck/.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(initial) | patch
Update from HH
authorCezary Kaliszyk <cek@colo12-c703.uibk.ac.at>
Mon, 26 Aug 2013 15:43:31 +0000 (17:43 +0200)
committerCezary Kaliszyk <cek@colo12-c703.uibk.ac.at>
Mon, 26 Aug 2013 15:43:31 +0000 (17:43 +0200)
commit4959bbf56f639e0c6a19eb9745f45223505135b9
tree074c03ca1772f4bd76431c902ec6aeeb4043048dtree | snapshot
Update from HH
663 files changed:
development/thales/chaff/august9_2011_session.hl [new file with mode: 0644] blob
development/thales/chaff/external_arith.hl [new file with mode: 0644] blob
development/thales/chaff/general/flyshot.hl [new file with mode: 0644] blob
development/thales/chaff/general/flyshot2.hl [new file with mode: 0644] blob
development/thales/chaff/general/flyspeck_utility.hl [new file with mode: 0644] blob
development/thales/chaff/general/generate_definitions.ml [new file with mode: 0644] blob
development/thales/chaff/general/log.hl [new file with mode: 0644] blob
development/thales/chaff/general/snapshot.hl [new file with mode: 0644] blob
development/thales/chaff/general/template_def.ml [new file with mode: 0644] blob
development/thales/chaff/general/xx.hl [new file with mode: 0644] blob
development/thales/chaff/load_path.ml [new file with mode: 0644] blob
development/thales/chaff/meson_edit.hl [new file with mode: 0644] blob
development/thales/chaff/tactic.hl [new file with mode: 0644] blob
development/thales/chaff/tactics.hl [new file with mode: 0644] blob
development/thales/chaff/tame_constants.ml [new file with mode: 0644] blob
development/thales/chaff/tmp/determinants_patch.ml [new file with mode: 0644] blob
development/thales/chaff/tmp/vectors_patch.ml [new file with mode: 0644] blob
development/thales/examples/axiom_example.hl [new file with mode: 0644] blob
development/thales/examples/beta_pair_thm.hl [new file with mode: 0644] blob
development/thales/examples/lemma_negligible.hl [new file with mode: 0644] blob
development/thales/examples/sierpinski.hl [new file with mode: 0644] blob
development/thales/examples/workshop2010_beta_pair_thm.hl [new file with mode: 0644] blob
development/thales/examples/workshop2010_ky_lemma_negligible.hl [new file with mode: 0644] blob
development/thales/examples/workshop2010_quyen_example.hl [new file with mode: 0644] blob
development/thales/log/log_searches.hl [new file with mode: 0644] blob
development/thales/ocaml/leech.ml [new file with mode: 0755] blob
development/thales/ocaml/rank_boost.hl [new file with mode: 0644] blob
development/thales/ocaml/script.ml [new file with mode: 0644] blob
development/thales/ocaml/sphere.ml [new file with mode: 0644] blob
development/thales/session/cleanup.hl [new file with mode: 0644] blob
development/thales/session/experiment_.hl [new file with mode: 0644] blob
development/thales/session/localbuild.hl [new file with mode: 0644] blob
development/thales/session/scratch.hl [new file with mode: 0644] blob
development/thales/session/work_in_progress.hl [new file with mode: 0644] blob
emacs/print-types.ml [new file with mode: 0644] blob
formal_ineqs/arith/arith_cache.hl [new file with mode: 0644] blob
formal_ineqs/arith/arith_num.hl [new file with mode: 0644] blob
formal_ineqs/arith/eval_interval.hl [new file with mode: 0644] blob
formal_ineqs/arith/float.hl [new file with mode: 0644] blob
formal_ineqs/arith/float_atn.hl [new file with mode: 0644] blob
formal_ineqs/arith/float_theory.hl [new file with mode: 0644] blob
formal_ineqs/arith/interval_arith.hl [new file with mode: 0644] blob
formal_ineqs/arith/more_float.hl [new file with mode: 0644] blob
formal_ineqs/arith/nat.hl [new file with mode: 0644] blob
formal_ineqs/arith/num_exp_theory.hl [new file with mode: 0644] blob
formal_ineqs/arith_options.hl [new file with mode: 0644] blob
formal_ineqs/examples.hl [new file with mode: 0644] blob
formal_ineqs/examples_flyspeck.hl [new file with mode: 0644] blob
formal_ineqs/examples_poly.hl [new file with mode: 0644] blob
formal_ineqs/informal/informal_arith.hl [new file with mode: 0644] blob
formal_ineqs/informal/informal_eval_interval.hl [new file with mode: 0644] blob
formal_ineqs/informal/informal_m_taylor.hl [new file with mode: 0644] blob
formal_ineqs/informal/informal_m_verifier.hl [new file with mode: 0644] blob
formal_ineqs/jordan/parse_ext_override_interface.hl [new file with mode: 0644] blob
formal_ineqs/jordan/real_ext.hl [new file with mode: 0644] blob
formal_ineqs/jordan/refinement.hl [new file with mode: 0644] blob
formal_ineqs/jordan/taylor_atn.hl [new file with mode: 0644] blob
formal_ineqs/lib/ssrbool-compiled.hl [new file with mode: 0644] blob
formal_ineqs/lib/ssreflect/sections.hl [new file with mode: 0644] blob
formal_ineqs/lib/ssreflect/ssreflect.hl [new file with mode: 0644] blob
formal_ineqs/lib/ssrfun-compiled.hl [new file with mode: 0644] blob
formal_ineqs/lib/ssrnat-compiled.hl [new file with mode: 0644] blob
formal_ineqs/list/list_conversions.hl [new file with mode: 0644] blob
formal_ineqs/list/list_float.hl [new file with mode: 0644] blob
formal_ineqs/list/more_list.hl [new file with mode: 0644] blob
formal_ineqs/misc/misc.hl [new file with mode: 0644] blob
formal_ineqs/misc/vars.hl [new file with mode: 0644] blob
formal_ineqs/taylor/m_taylor.hl [new file with mode: 0644] blob
formal_ineqs/taylor/m_taylor_arith.hl [new file with mode: 0644] blob
formal_ineqs/taylor/m_taylor_arith2.hl [new file with mode: 0644] blob
formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl [new file with mode: 0644] blob
formal_ineqs/taylor/theory/taylor_interval-compiled.hl [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/interval.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/line_interval.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/recurse.hl [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/recurse.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/recurse0.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/report.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/taylor.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/types.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/univariate.ml [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/verifier.hl [new file with mode: 0644] blob
formal_ineqs/verifier/interval_m/verifier.ml [new file with mode: 0644] blob
formal_ineqs/verifier/m_verifier.hl [new file with mode: 0644] blob
formal_ineqs/verifier/m_verifier_build.hl [new file with mode: 0644] blob
formal_ineqs/verifier/m_verifier_main.hl [new file with mode: 0644] blob
formal_ineqs/verifier_options.hl [new file with mode: 0644] blob
formal_lp/glpk/build_certificates.hl [new file with mode: 0644] blob
formal_lp/glpk/build_main.hl [new file with mode: 0644] blob
formal_lp/glpk/ex1/bb1_out.hl [new file with mode: 0644] blob
formal_lp/glpk/ex2/bb2_1_out.hl [new file with mode: 0644] blob
formal_lp/glpk/ex2/bb2_2_out.hl [new file with mode: 0644] blob
formal_lp/glpk/ex2/bb2_3_out.hl [new file with mode: 0644] blob
formal_lp/glpk/ex2/bb2_4_out.hl [new file with mode: 0644] blob
formal_lp/glpk/ex2/bb2_5_out.hl [new file with mode: 0644] blob
formal_lp/glpk/feasible.hl [new file with mode: 0644] blob
formal_lp/glpk/lp_binary_certificate.hl [new file with mode: 0644] blob
formal_lp/glpk/onepass.hl [new file with mode: 0644] blob
formal_lp/glpk/test_hard.hl [new file with mode: 0644] blob
formal_lp/hypermap/arith_link.hl [new file with mode: 0644] blob
formal_lp/hypermap/computations/informal_computations.hl [new file with mode: 0644] blob
formal_lp/hypermap/computations/list_conversions2.hl [new file with mode: 0644] blob
formal_lp/hypermap/computations/list_hypermap_computations.hl [new file with mode: 0644] blob
formal_lp/hypermap/computations/more_theory-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_approx_ineqs.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_body_ineqs.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_body_ineqs_data.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_gen_ineqs.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_gen_theory-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_head_ineqs.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_ineqs.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_ineqs_defs.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/main/lp_certificate.hl [new file with mode: 0644] blob
formal_lp/hypermap/main/prove_flyspeck_lp.hl [new file with mode: 0644] blob
formal_lp/hypermap/main/test6.hl [new file with mode: 0644] blob
formal_lp/hypermap/main/test_ex2_complete.hl [new file with mode: 0644] blob
formal_lp/hypermap/main/test_hard.hl [new file with mode: 0644] blob
formal_lp/hypermap/ssreflect/add_triangle-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/ssreflect/list_hypermap-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/ssreflect/list_hypermap_iso-compiled.hl [new file with mode: 0644] blob
formal_lp/hypermap/tests/test_all_lists.hl [new file with mode: 0644] blob
formal_lp/hypermap/verify_all.hl [new file with mode: 0644] blob
formal_lp/ineqs/constants_approx.hl [new file with mode: 0644] blob
formal_lp/ineqs/delta_ineq.hl [new file with mode: 0644] blob
formal_lp/lp_example/out_test.hl [new file with mode: 0644] blob
formal_lp/more_arith/arith_int.hl [new file with mode: 0644] blob
formal_lp/more_arith/lin_f.hl [new file with mode: 0644] blob
formal_lp/more_arith/prove_lp.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_array.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_cache.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_hash.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_hash2.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_hash_int.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_hash_rat.hl [new file with mode: 0644] blob
formal_lp/old/arith/arith_options.hl [new file with mode: 0644] blob
formal_lp/old/arith/float.hl [new file with mode: 0644] blob
formal_lp/old/arith/float_atn.hl [new file with mode: 0644] blob
formal_lp/old/arith/float_test.hl [new file with mode: 0644] blob
formal_lp/old/arith/float_theory.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/informal_arith.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/informal_eval_interval.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/informal_m_taylor.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/informal_m_verifier.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/tests1.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/tests2.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/tests3.hl [new file with mode: 0644] blob
formal_lp/old/arith/informal/tests_poly.hl [new file with mode: 0644] blob
formal_lp/old/arith/interval_arith.hl [new file with mode: 0644] blob
formal_lp/old/arith/misc.hl [new file with mode: 0644] blob
formal_lp/old/arith/nat.hl [new file with mode: 0644] blob
formal_lp/old/arith/num_exp_theory.hl [new file with mode: 0644] blob
formal_lp/old/arith/prove_lp.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data10.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data15.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data18.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data20.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data25.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data27.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/arith_test_data5.hl [new file with mode: 0644] blob
formal_lp/old/arith/tests/test_nat_arith.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/eval_interval.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/interval.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/line_interval.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/recurse.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/report.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/taylor.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/test1d.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/types.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_1d/univariate.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/function_data.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/interval.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/line_interval.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/recurse.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/recurse0.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/report.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/taylor.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/types.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/univariate.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/interval_m/verifier.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/lin_approx.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_examples_poly.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_taylor.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_taylor_arith.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_taylor_arith2.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_taylor_old.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_test.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_tests.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_tests2.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_tests3.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_tests4.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_verifier.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/m_verifier0.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/more_float.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/second_approx.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/test.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/test_taylor_arith.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/tests_cmp.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/theory/multivariate_taylor.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/theory/taylor_interval.hl [new file with mode: 0644] blob
formal_lp/old/formal_interval/verifier.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/constants_approx.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/contravening_ineqs.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/list_conversions.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/list_hypermap.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/list_hypermap_computations.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/list_hypermap_defs.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/list_hypermap_iso.hl [new file with mode: 0644] blob
formal_lp/old/hypermap/nobranching_lp.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/contravening_ineqs.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/list_conversions.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/list_hypermap.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/list_hypermap_computations.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/list_hypermap_defs.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/list_hypermap_iso.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/list_hypermap_vars.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/nobranching_lp.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/149438122187_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/156588677070_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/168941837467_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/176747399778_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/196565289721_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/202328731904_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/204898223616_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/206221606034_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/209986500083_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/234860659776_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/241242841715_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/241966209046_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/28820130324_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/62059307362_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/63917576180_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/72977109430_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/75655754509_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/86324340346_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/95170601659_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/97685954266_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/all.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests/all_tests.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/118343205068_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/118760185161_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/119040238600_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/122526068934_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/123040027899_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/125719999821_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/147671934133_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/156401568298_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/156615503428_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/158856256118_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/165950391005_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/168156828154_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/17272290668_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/195482381558_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/196021155893_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/206084941231_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/211626865969_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/219955817888_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/245859035526_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/25168582633_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/30500231120_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/4436579732_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/63626063287_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/69964410750_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/74394196986_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/91057093091_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/945145744_out.hl [new file with mode: 0644] blob
formal_lp/old/ineqs/tests2/all_tests.hl [new file with mode: 0644] blob
formal_lp/old/list/list_conversions.hl [new file with mode: 0644] blob
formal_lp/old/list/list_float.hl [new file with mode: 0644] blob
glpk/glpk_link.ml [new file with mode: 0644] blob
glpk/minorlp/OXLZLEZ.ml [new file with mode: 0644] blob
glpk/minorlp/tame_table.ml [new file with mode: 0644] blob
glpk/sphere.ml [new file with mode: 0644] blob
glpk/tame_archive/build_lp.hl [new file with mode: 0644] blob
glpk/tame_archive/hard_lp.ml [new file with mode: 0644] blob
glpk/tame_archive/lpproc.ml [new file with mode: 0644] blob
glpk/tame_archive/scaffolding.hl [new file with mode: 0644] blob
graph_generator/graph_control.hl [new file with mode: 0644] blob
jHOLLight/Examples/group_sylow-compiled.hl [new file with mode: 0644] blob
jHOLLight/Examples/seq-compiled.hl [new file with mode: 0644] blob
jHOLLight/Examples/ssrbool-compiled.hl [new file with mode: 0644] blob
jHOLLight/Examples/ssrfun-compiled.hl [new file with mode: 0644] blob
jHOLLight/Examples/ssrnat-compiled.hl [new file with mode: 0644] blob
jHOLLight/JHOL.app/Contents/Resources/Java/newprinter.ml [new file with mode: 0644] blob
jHOLLight/caml/raw_printer.hl [new file with mode: 0644] blob
jHOLLight/caml/sections.hl [new file with mode: 0644] blob
jHOLLight/caml/ssreflect.hl [new file with mode: 0644] blob
kepler_tex/tikz/tikz.ml [new file with mode: 0644] blob
legacy/general/database_more.ml [new file with mode: 0644] blob
legacy/general/deprecated_sphere.hl [new file with mode: 0644] blob
legacy/glpk/glpk/glpk_def.hl [new file with mode: 0644] blob
legacy/glpk/glpk/mkineq.ml [new file with mode: 0644] blob
legacy/glpk/glpk/tame_archive_hard_notes.hl [new file with mode: 0644] blob
legacy/inequalities/definitions_kepler.ml [new file with mode: 0644] blob
legacy/inequalities/definitions_keplerC.ml [new file with mode: 0644] blob
legacy/inequalities/dodec_ineq_names.ml [new file with mode: 0644] blob
legacy/inequalities/dodec_inequalities.ml [new file with mode: 0644] blob
legacy/inequalities/generate-ineq-syntax.ml [new file with mode: 0644] blob
legacy/inequalities/inequality_spec.ml [new file with mode: 0644] blob
legacy/inequalities/kep_deprecated.ml [new file with mode: 0644] blob
legacy/inequalities/kep_ineq_bis.ml [new file with mode: 0644] blob
legacy/inequalities/kep_inequalities.ml [new file with mode: 0644] blob
legacy/inequalities/kep_inequalities2.ml [new file with mode: 0644] blob
legacy/inequalities/kepler_ineq_names.ml [new file with mode: 0644] blob
legacy/inequalities/ocaml_to_sml.ml [new file with mode: 0644] blob
legacy/inequalities/sigmahat.hl [new file with mode: 0644] blob
legacy/inequalities/sphere.ml [new file with mode: 0644] blob
legacy/linear_program/LinProg.ml [new file with mode: 0644] blob
legacy/load_def_kepler.ml [new file with mode: 0644] blob
legacy/oldfan/Conforming2.hl [new file with mode: 0644] blob
legacy/oldfan/DHVFGBC.hl [new file with mode: 0755] blob
legacy/oldfan/DWWUTKW.hl [new file with mode: 0755] blob
legacy/oldfan/IBZWFFH.hl [new file with mode: 0755] blob
legacy/oldfan/JBDNJJB.hl [new file with mode: 0755] blob
legacy/oldfan/JGIYDLE.hl [new file with mode: 0755] blob
legacy/oldfan/JUTSTKG.hl [new file with mode: 0755] blob
legacy/oldfan/LEMMA.hl [new file with mode: 0755] blob
legacy/oldfan/RWXUYZZ.hl [new file with mode: 0755] blob
legacy/oldfan/TACTIC.hl [new file with mode: 0644] blob
legacy/oldfan/ULEKUUB.hl [new file with mode: 0755] blob
legacy/oldfan/VBTIKLP.hl [new file with mode: 0755] blob
legacy/oldfan/ch_fan/FAN_DEF.ml [new file with mode: 0644] blob
legacy/oldfan/ch_fan/fan_definition.hl [new file with mode: 0644] blob
legacy/oldfan/ch_fan/fan_definition2.hl [new file with mode: 0644] blob
legacy/oldfan/ch_fan/fan_summary.hl [new file with mode: 0644] blob
legacy/oldfan/definition_fan.hl [new file with mode: 0755] blob
legacy/oldfan/fan_concl.hl [new file with mode: 0644] blob
legacy/oldfan/fantopology.ml [new file with mode: 0644] blob
legacy/oldfan/fully_surrounded.hl [new file with mode: 0755] blob
legacy/oldfan/hypermap_of_fan.hl [new file with mode: 0755] blob
legacy/oldfan/introduction1.hl [new file with mode: 0755] blob
legacy/oldfan/leads_into.hl [new file with mode: 0755] blob
legacy/oldfan/node_fan.hl [new file with mode: 0755] blob
legacy/oldhypermap/ch_hypermap/hypermap_summary.hl [new file with mode: 0644] blob
legacy/oldleg/assembly.ml [new file with mode: 0644] blob
legacy/oldleg/collect_geom.ml [new file with mode: 0644] blob
legacy/oldleg/collect_geom_a.ml [new file with mode: 0644] blob
legacy/oldleg/collect_geom_error.ml [new file with mode: 0644] blob
legacy/oldleg/collect_geom_spec.ml [new file with mode: 0644] blob
legacy/oldleg/geomdetail.ml [new file with mode: 0644] blob
legacy/oldleg/geomdetail_08.ml [new file with mode: 0644] blob
legacy/oldleg/hull.ml [new file with mode: 0644] blob
legacy/oldleg/hull_error.ml [new file with mode: 0644] blob
legacy/oldlocal/PQCSXWG_old.hl [new file with mode: 0644] blob
legacy/oldlocal/XBJRPHC.hl [new file with mode: 0644] blob
legacy/oldlocal/ch_local/CKQOWSA.hl [new file with mode: 0644] blob
legacy/oldlocal/ch_local/cyclic_definition.hl [new file with mode: 0644] blob
legacy/oldlocal/ch_local/local_defs.hl [new file with mode: 0644] blob
legacy/oldlocal/ch_local/local_defs2.hl [new file with mode: 0644] blob
legacy/oldlocal/ch_local/local_fan.ml [new file with mode: 0644] blob
legacy/oldlocal/nguyenquangtruong270983/JBDNJJB.hl [new file with mode: 0644] blob
legacy/oldlocal/nguyenquangtruong270983/WRGCVDR_CIZMRRH.hl [new file with mode: 0644] blob
legacy/oldnonlinear/cutlemmas.hl [new file with mode: 0644] blob
legacy/oldnonlinear/deprecated_main_estimate_ineq.hl [new file with mode: 0644] blob
legacy/oldnonlinear/mdtau.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/break_quad_jul2013.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/experiments/oracle.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/experiments/test.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/experiments/test_may_2012.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/experiments/zumkeller_test.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/fejestoth12.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/ineq_cell23.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/main_estimate_pent_hex_cut_may_2013.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/main_ineq_calcs.ml [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/partials.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/temp_ineq.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/test_ineq.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/test_jun2012_ZTG_series.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/test_may2013_terminal_pent_hex_series.hl [new file with mode: 0644] blob
legacy/oldnonlinear/nonlinear/text_interface.hl [new file with mode: 0644] blob
legacy/oldnonlinear/post.hl [new file with mode: 0644] blob
legacy/oldnonlinear/removedef.hl [new file with mode: 0644] blob
legacy/oldpacking/BBDTRGC_def.hl [new file with mode: 0644] blob
legacy/oldpacking/DRUQUFE.hl [new file with mode: 0644] blob
legacy/oldpacking/IDBEZAL.hl [new file with mode: 0644] blob
legacy/oldpacking/JJGTQMN_def.hl [new file with mode: 0644] blob
legacy/oldpacking/JNRJQSM_def.hl [new file with mode: 0644] blob
legacy/oldpacking/KHEJKCI.hl [new file with mode: 0644] blob
legacy/oldpacking/NOPZSEH_def.hl [new file with mode: 0644] blob
legacy/oldpacking/PHZVPFY_def.hl [new file with mode: 0644] blob
legacy/oldpacking/RHWVGNP.hl [new file with mode: 0644] blob
legacy/oldpacking/TIWWFYQ.hl [new file with mode: 0644] blob
legacy/oldpacking/ch_packing/TSKAJXY.hl [new file with mode: 0644] blob
legacy/oldpacking/ch_packing/oxl_lemma.hl [new file with mode: 0644] blob
legacy/oldpacking/ky_packing/EMNWUUS.hl [new file with mode: 0644] blob
legacy/oldpacking/ky_packing/UPFZBZM.hl [new file with mode: 0644] blob
legacy/oldpacking/ky_packing/UPFZBZM_axioms.hl [new file with mode: 0644] blob
legacy/oldpacking/ky_packing/UPFZBZM_support_lemmas.hl [new file with mode: 0644] blob
legacy/oldpacking/ky_packing/UPFZBZM_working.hl [new file with mode: 0644] blob
legacy/oldpacking/ky_packing/marchal_cells.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/GRUTOTI.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/KIZHLTL.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/RDWKARC.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/UPFZBZM.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/load_sequence.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/marchal_cells_3.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/Backup/sum_gammaX_lmfun_estimate.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/REUHADY.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/TSKAJXY.hl [new file with mode: 0644] blob
legacy/oldpacking/packing/development/marchal_cells_2.hl [new file with mode: 0755] blob
legacy/oldpacking/packing/development/sum_beta_bump.hl [new file with mode: 0755] blob
legacy/oldpacking/packing/development/working.hl [new file with mode: 0644] blob
legacy/oldtame/UBHDEUU.hl [new file with mode: 0644] blob
legacy/oldtame/dangtatdatusb/DLWCHEM.hl [new file with mode: 0644] blob
legacy/oldtame/dangtatdatusb/UBHDEUU.hl [new file with mode: 0644] blob
legacy/oldtame/pishort.hl [new file with mode: 0644] blob
legacy/oldtame/quarantine/SZIPOAS.hl [new file with mode: 0644] blob
legacy/oldtrig/run_file_euler.ml [new file with mode: 0755] blob
legacy/oldtrig/trig_old.ml [new file with mode: 0644] blob
legacy/oldvolume/ch_volume/vol2.hl [new file with mode: 0644] blob
legacy/oldvolume/ch_volume/volume.hl [new file with mode: 0644] blob
legacy/oldvolume/ch_volume/volume_temp.hl [new file with mode: 0644] blob
legacy/toplevel.ml [new file with mode: 0644] blob
make.ml [new file with mode: 0644] blob
port_interval/compose.hl [new file with mode: 0644] blob
port_interval/function_data.hl [new file with mode: 0644] blob
port_interval/interval.hl [new file with mode: 0644] blob
port_interval/line_interval.hl [new file with mode: 0644] blob
port_interval/recurse.hl [new file with mode: 0644] blob
port_interval/report.hl [new file with mode: 0644] blob
port_interval/taylor.hl [new file with mode: 0644] blob
port_interval/types.hl [new file with mode: 0644] blob
port_interval/univariate.hl [new file with mode: 0644] blob
projects_discrete_geom/bcc_lattice.hl [new file with mode: 0644] blob
projects_discrete_geom/bezdek_reid/bezdek_reid.hl [new file with mode: 0644] blob
projects_discrete_geom/fejestoth12/defs.hl [new file with mode: 0644] blob
projects_discrete_geom/fejestoth12/lipstick_ft.ml [new file with mode: 0644] blob
projects_discrete_geom/strong_dodec_conj/strongdodec_ineq.hl [new file with mode: 0644] blob
tame_archive/tame_archive.hl [new file with mode: 0644] blob
text_formalization/boot.hl [new file with mode: 0644] blob
text_formalization/boot.ml [new file with mode: 0644] blob
text_formalization/build.hl [new file with mode: 0644] blob
text_formalization/computational_build.hl [new file with mode: 0644] blob
text_formalization/fan/CFYXFTY.hl [new file with mode: 0644] blob
text_formalization/fan/Conforming.hl [new file with mode: 0755] blob
text_formalization/fan/GMLWKPK.hl [new file with mode: 0644] blob
text_formalization/fan/HypermapAndFan.hl [new file with mode: 0644] blob
text_formalization/fan/fan_defs.hl [new file with mode: 0644] blob
text_formalization/fan/fan_misc.hl [new file with mode: 0644] blob
text_formalization/fan/hypermap_iso-compiled.hl [new file with mode: 0644] blob
text_formalization/fan/introduction.hl [new file with mode: 0755] blob
text_formalization/fan/planarity.hl [new file with mode: 0755] blob
text_formalization/fan/polyhedron.hl [new file with mode: 0644] blob
text_formalization/fan/topology.hl [new file with mode: 0755] blob
text_formalization/general/debug.hl [new file with mode: 0644] blob
text_formalization/general/flyspeck_lib.hl [new file with mode: 0644] blob
text_formalization/general/hol_pervasives.hl [new file with mode: 0644] blob
text_formalization/general/lib.hl [new file with mode: 0644] blob
text_formalization/general/package_constant.hl [new file with mode: 0644] blob
text_formalization/general/parser_verbose.hl [new file with mode: 0644] blob
text_formalization/general/print_types.hl [new file with mode: 0644] blob
text_formalization/general/prove_by_refinement.hl [new file with mode: 0644] blob
text_formalization/general/sphere.hl [new file with mode: 0644] blob
text_formalization/general/state_manager.hl [new file with mode: 0644] blob
text_formalization/general/tactics.hl [new file with mode: 0644] blob
text_formalization/general/update_database_310.ml [new file with mode: 0644] blob
text_formalization/general/update_database_400.ml [new file with mode: 0644] blob
text_formalization/hypermap/bauer_nipkow.hl [new file with mode: 0644] blob
text_formalization/hypermap/hypermap.hl [new file with mode: 0644] blob
text_formalization/hypermap/summary.hl [new file with mode: 0644] blob
text_formalization/jordan/compute_pi.hl [new file with mode: 0644] blob
text_formalization/jordan/float.hl [new file with mode: 0644] blob
text_formalization/jordan/float_example.hl [new file with mode: 0644] blob
text_formalization/jordan/flyspeck_constants.hl [new file with mode: 0644] blob
text_formalization/jordan/goal_printer.hl [new file with mode: 0644] blob
text_formalization/jordan/hash_term.hl [new file with mode: 0644] blob
text_formalization/jordan/lib_ext.hl [new file with mode: 0644] blob
text_formalization/jordan/make.hl [new file with mode: 0644] blob
text_formalization/jordan/misc_defs_and_lemmas.hl [new file with mode: 0644] blob
text_formalization/jordan/num_ext_gcd.hl [new file with mode: 0644] blob
text_formalization/jordan/num_ext_nabs.hl [new file with mode: 0644] blob
text_formalization/jordan/parse_ext_override_interface.hl [new file with mode: 0644] blob
text_formalization/jordan/real_ext.hl [new file with mode: 0644] blob
text_formalization/jordan/real_ext_geom_series.hl [new file with mode: 0644] blob
text_formalization/jordan/refinement.hl [new file with mode: 0644] blob
text_formalization/jordan/tactics_jordan.hl [new file with mode: 0644] blob
text_formalization/jordan/taylor_atn.hl [new file with mode: 0644] blob
text_formalization/leg/AFF_SGN_TAC.hl [new file with mode: 0644] blob
text_formalization/leg/abc_of_quadratic_def.hl [new file with mode: 0644] blob
text_formalization/leg/affprops.hl [new file with mode: 0644] blob
text_formalization/leg/basics.hl [new file with mode: 0644] blob
text_formalization/leg/cayleyR_def.hl [new file with mode: 0644] blob
text_formalization/leg/collect_geom.hl [new file with mode: 0644] blob
text_formalization/leg/collect_geom2.hl [new file with mode: 0644] blob
text_formalization/leg/enclosed_def.hl [new file with mode: 0644] blob
text_formalization/leg/geomdetail.hl [new file with mode: 0644] blob
text_formalization/leg/muR_def.hl [new file with mode: 0644] blob
text_formalization/leg/quadratic_root_plus_def.hl [new file with mode: 0644] blob
text_formalization/local/ARDBZYE.hl [new file with mode: 0644] blob
text_formalization/local/AUEAHEH.hl [new file with mode: 0644] blob
text_formalization/local/AURSIPD.hl [new file with mode: 0644] blob
text_formalization/local/AXJRPNC.hl [new file with mode: 0644] blob
text_formalization/local/AYQJTMD.hl [new file with mode: 0755] blob
text_formalization/local/BKOSSGE.hl [new file with mode: 0644] blob
text_formalization/local/CNICGSF.hl [new file with mode: 0644] blob
text_formalization/local/CQAOQLR.hl [new file with mode: 0644] blob
text_formalization/local/CUXVZOZ.hl [new file with mode: 0644] blob
text_formalization/local/EYYPQDW.hl [new file with mode: 0755] blob
text_formalization/local/FEKTYIY.hl [new file with mode: 0644] blob
text_formalization/local/GBYCPXS.hl [new file with mode: 0755] blob
text_formalization/local/HDPLYGY.hl [new file with mode: 0755] blob
text_formalization/local/HIJQAHA.hl [new file with mode: 0644] blob
text_formalization/local/HXHYTIJ.hl [new file with mode: 0755] blob
text_formalization/local/IMJXPHR.hl [new file with mode: 0755] blob
text_formalization/local/IUNBUIG.hl [new file with mode: 0644] blob
text_formalization/local/JCYFMRP.hl [new file with mode: 0644] blob
text_formalization/local/JEJTVGB.hl [new file with mode: 0644] blob
text_formalization/local/JKQEWGV.hl [new file with mode: 0755] blob
text_formalization/local/JLXFDMJ.hl [new file with mode: 0644] blob
text_formalization/local/JOTSWIX.hl [new file with mode: 0644] blob
text_formalization/local/LDURDPN.hl [new file with mode: 0644] blob
text_formalization/local/LFJCIXP.hl [new file with mode: 0644] blob
text_formalization/local/LKGRQUI.hl [new file with mode: 0755] blob
text_formalization/local/LOCAL_LEMMAS.hl [new file with mode: 0644] blob
text_formalization/local/LVDUCXU.hl [new file with mode: 0644] blob
text_formalization/local/MIQMCSN.hl [new file with mode: 0644] blob
text_formalization/local/MTUWLUN.hl [new file with mode: 0755] blob
text_formalization/local/NKEZBFC.hl [new file with mode: 0644] blob
text_formalization/local/NUXCOEA.hl [new file with mode: 0644] blob
text_formalization/local/OCBICBY.hl [new file with mode: 0644] blob
text_formalization/local/ODXLSTCv2.hl [new file with mode: 0755] blob
text_formalization/local/OTMTOTJ.hl [new file with mode: 0644] blob
text_formalization/local/PCRTTID.hl [new file with mode: 0644] blob
text_formalization/local/PPBTYDQ.hl [new file with mode: 0644] blob
text_formalization/local/PQCSXWG.hl [new file with mode: 0644] blob
text_formalization/local/QKNVMLB.hl [new file with mode: 0755] blob
text_formalization/local/RNSYJXM-compiled.hl [new file with mode: 0644] blob
text_formalization/local/RRCWNSJ.hl [new file with mode: 0644] blob
text_formalization/local/SGTRNAF.hl [new file with mode: 0755] blob
text_formalization/local/TECOXBM.hl [new file with mode: 0644] blob
text_formalization/local/TFITSKC.hl [new file with mode: 0644] blob
text_formalization/local/UAGHHBM.hl [new file with mode: 0755] blob
text_formalization/local/UXCKFPE.hl [new file with mode: 0755] blob
text_formalization/local/VASYYAU.hl [new file with mode: 0644] blob
text_formalization/local/VPWSHTO.hl [new file with mode: 0644] blob
text_formalization/local/WJSCPRO.hl [new file with mode: 0755] blob
text_formalization/local/WKEIDFT.hl [new file with mode: 0644] blob
text_formalization/local/WRGCVDR_CIZMRRH.hl [new file with mode: 0644] blob
text_formalization/local/XIVPHKS.hl [new file with mode: 0644] blob
text_formalization/local/XWITCCN.hl [new file with mode: 0755] blob
text_formalization/local/YRTAFYH.hl [new file with mode: 0644] blob
text_formalization/local/YXIONXL.hl [new file with mode: 0755] blob
text_formalization/local/YXIONXL2.hl [new file with mode: 0755] blob
text_formalization/local/ZITHLQN.hl [new file with mode: 0644] blob
text_formalization/local/ZLZTHIC.hl [new file with mode: 0644] blob
text_formalization/local/appendix_main_estimate.hl [new file with mode: 0644] blob
text_formalization/local/deformation.hl [new file with mode: 0644] blob
text_formalization/local/dih2k.hl [new file with mode: 0755] blob
text_formalization/local/hexagons.hl [new file with mode: 0644] blob
text_formalization/local/local_lemmas1.hl [new file with mode: 0644] blob
text_formalization/local/localization.hl [new file with mode: 0644] blob
text_formalization/local/lp_details.hl [new file with mode: 0644] blob
text_formalization/local/lunar_deform.hl [new file with mode: 0644] blob
text_formalization/local/pent_hex.hl [new file with mode: 0644] blob
text_formalization/local/polar_fan.hl [new file with mode: 0644] blob
text_formalization/local/terminal.hl [new file with mode: 0644] blob
text_formalization/nonlinear/auto_lib.hl [new file with mode: 0644] blob
text_formalization/nonlinear/break_case_exec.hl [new file with mode: 0644] blob
text_formalization/nonlinear/break_case_log.hl [new file with mode: 0644] blob
text_formalization/nonlinear/calc_derivative.hl [new file with mode: 0644] blob
text_formalization/nonlinear/check_completeness.hl [new file with mode: 0644] blob
text_formalization/nonlinear/cleanDeriv.hl [new file with mode: 0644] blob
text_formalization/nonlinear/cleanDeriv_examples.hl [new file with mode: 0644] blob
text_formalization/nonlinear/compute_2158872499.hl [new file with mode: 0644] blob
text_formalization/nonlinear/formal_tests/hminus.hl [new file with mode: 0644] blob
text_formalization/nonlinear/formal_tests/ineq_ids.hl [new file with mode: 0644] blob
text_formalization/nonlinear/formal_tests/load.hl [new file with mode: 0644] blob
text_formalization/nonlinear/formal_tests/test1.hl [new file with mode: 0644] blob
text_formalization/nonlinear/formal_tests/test2.hl [new file with mode: 0644] blob
text_formalization/nonlinear/function_list.hl [new file with mode: 0644] blob
text_formalization/nonlinear/functional_equation.hl [new file with mode: 0644] blob
text_formalization/nonlinear/ineq.hl [new file with mode: 0644] blob
text_formalization/nonlinear/ineqdata3q1h.hl [new file with mode: 0644] blob
text_formalization/nonlinear/lemma.hl [new file with mode: 0644] blob
text_formalization/nonlinear/main_estimate_ineq.hl [new file with mode: 0644] blob
text_formalization/nonlinear/merge_ineq.hl [new file with mode: 0644] blob
text_formalization/nonlinear/mk_all_ineq.hl [new file with mode: 0644] blob
text_formalization/nonlinear/nonlin_def.hl [new file with mode: 0644] blob
text_formalization/nonlinear/optimize.hl [new file with mode: 0644] blob
text_formalization/nonlinear/parse_ineq.hl [new file with mode: 0644] blob
text_formalization/nonlinear/prep.hl [new file with mode: 0755] blob
text_formalization/nonlinear/scripts.hl [new file with mode: 0644] blob
text_formalization/nonlinear/sharp.hl [new file with mode: 0644] blob
text_formalization/nonlinear/types.hl [new file with mode: 0644] blob
text_formalization/nonlinear/vukhacky_tactics.hl [new file with mode: 0644] blob
text_formalization/packing/AJRIPQN.hl [new file with mode: 0755] blob
text_formalization/packing/DDZUPHJ.hl [new file with mode: 0755] blob
text_formalization/packing/EMNWUUS.hl [new file with mode: 0755] blob
text_formalization/packing/GRUTOTI.hl [new file with mode: 0755] blob
text_formalization/packing/HDTFNFZ.hl [new file with mode: 0755] blob
text_formalization/packing/KIZHLTL.hl [new file with mode: 0755] blob
text_formalization/packing/LEPJBDJ.hl [new file with mode: 0755] blob
text_formalization/packing/NJIUTIU.hl [new file with mode: 0755] blob
text_formalization/packing/OXLZLEZ.hl [new file with mode: 0644] blob
text_formalization/packing/OXL_def.hl [new file with mode: 0644] blob
text_formalization/packing/QZKSYKG.hl [new file with mode: 0755] blob
text_formalization/packing/QZYZMJC.hl [new file with mode: 0644] blob
text_formalization/packing/RDWKARC.hl [new file with mode: 0755] blob
text_formalization/packing/REUHADY.hl [new file with mode: 0644] blob
text_formalization/packing/RVFXZBU.hl [new file with mode: 0755] blob
text_formalization/packing/Rogers.hl [new file with mode: 0644] blob
text_formalization/packing/SLTSTLO.hl [new file with mode: 0755] blob
text_formalization/packing/TARJJUW.hl [new file with mode: 0644] blob
text_formalization/packing/TEZFFSK.hl [new file with mode: 0755] blob
text_formalization/packing/TSKAJXY.hl [new file with mode: 0644] blob
text_formalization/packing/TSKAJXY_034.hl [new file with mode: 0644] blob
text_formalization/packing/TSKAJXY_lemmas.hl [new file with mode: 0644] blob
text_formalization/packing/UPFZBZM.hl [new file with mode: 0755] blob
text_formalization/packing/UPFZBZM_support_lemmas.hl [new file with mode: 0755] blob
text_formalization/packing/URRPHBZ1.hl [new file with mode: 0644] blob
text_formalization/packing/URRPHBZ2.hl [new file with mode: 0755] blob
text_formalization/packing/URRPHBZ3.hl [new file with mode: 0755] blob
text_formalization/packing/YNHYJIT.hl [new file with mode: 0755] blob
text_formalization/packing/YSSKQOY.hl [new file with mode: 0644] blob
text_formalization/packing/bump.hl [new file with mode: 0644] blob
text_formalization/packing/counting_spheres.hl [new file with mode: 0644] blob
text_formalization/packing/leaf_cell.hl [new file with mode: 0644] blob
text_formalization/packing/marchal_cells.hl [new file with mode: 0755] blob
text_formalization/packing/marchal_cells_2_new.hl [new file with mode: 0755] blob
text_formalization/packing/marchal_cells_3.hl [new file with mode: 0755] blob
text_formalization/packing/oxl_2012.hl [new file with mode: 0644] blob
text_formalization/packing/pack1.hl [new file with mode: 0644] blob
text_formalization/packing/pack2.hl [new file with mode: 0644] blob
text_formalization/packing/pack3.hl [new file with mode: 0644] blob
text_formalization/packing/pack_concl.hl [new file with mode: 0644] blob
text_formalization/packing/pack_defs.hl [new file with mode: 0644] blob
text_formalization/packing/sum_gammaX_lmfun_estimate.hl [new file with mode: 0755] blob
text_formalization/strictbuild.hl [new file with mode: 0644] blob
text_formalization/tame/ArcProperties.hl [new file with mode: 0644] blob
text_formalization/tame/CDTETAT.hl [new file with mode: 0644] blob
text_formalization/tame/CKQOWSA.hl [new file with mode: 0644] blob
text_formalization/tame/CKQOWSA_3.hl [new file with mode: 0644] blob
text_formalization/tame/CKQOWSA_4.hl [new file with mode: 0644] blob
text_formalization/tame/CRTTXAT.hl [new file with mode: 0644] blob
text_formalization/tame/FATUGPD.hl [new file with mode: 0755] blob
text_formalization/tame/HRXEFDM.hl [new file with mode: 0644] blob
text_formalization/tame/Inequalities.hl [new file with mode: 0644] blob
text_formalization/tame/JGTDEBU.hl [new file with mode: 0644] blob
text_formalization/tame/TameGeneral.hl [new file with mode: 0644] blob
text_formalization/tame/dont_repeat_yourself.hl [new file with mode: 0644] blob
text_formalization/tame/ssreflect/FNJLBXS-compiled.hl [new file with mode: 0644] blob
text_formalization/tame/ssreflect/KCBLRQC-compiled.hl [new file with mode: 0644] blob
text_formalization/tame/ssreflect/MQMSMAB-compiled.hl [new file with mode: 0644] blob
text_formalization/tame/ssreflect/seq2-compiled.hl [new file with mode: 0644] blob
text_formalization/tame/ssreflect/sort-compiled.hl [new file with mode: 0644] blob
text_formalization/tame/ssreflect/tame_lemmas-compiled.hl [new file with mode: 0644] blob
text_formalization/tame/tame_concl.hl [new file with mode: 0644] blob
text_formalization/tame/tame_defs.hl [new file with mode: 0644] blob
text_formalization/tame/tame_opposite.hl [new file with mode: 0644] blob
text_formalization/trigonometry/HVIHVEC.hl [new file with mode: 0644] blob
text_formalization/trigonometry/delta_x.hl [new file with mode: 0755] blob
text_formalization/trigonometry/euler_complement.hl [new file with mode: 0755] blob
text_formalization/trigonometry/euler_main_theorem.hl [new file with mode: 0755] blob
text_formalization/trigonometry/euler_multivariate.hl [new file with mode: 0755] blob
text_formalization/trigonometry/trig1.hl [new file with mode: 0644] blob
text_formalization/trigonometry/trig2.hl [new file with mode: 0644] blob
text_formalization/trigonometry/trigonometry.hl [new file with mode: 0644] blob
text_formalization/usr/thales/hales_tactic.hl [new file with mode: 0644] blob
text_formalization/usr/thales/init_search.hl [new file with mode: 0644] blob
text_formalization/usr/thales/searching.hl [new file with mode: 0644] blob
text_formalization/volume/vol1.hl [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.