05bd666 | zipperer | 26 November 2020, 19:53:58 UTC | minuscule edits (#5) * edit README - replace 'stament' with 'statement' * Edit build.hl -- add period at end of sentence | 26 November 2020, 19:53:58 UTC |
24d2c55 | Alexey Solovyev | 18 September 2019, 23:09:23 UTC | Misc | 18 September 2019, 23:09:23 UTC |
a2637fc | Alexey Solovyev | 18 September 2019, 06:01:20 UTC | INSTALL: native compilation | 18 September 2019, 06:01:20 UTC |
0c5e873 | Alexey Solovyev | 18 September 2019, 05:47:49 UTC | INSTALL.md | 18 September 2019, 05:47:49 UTC |
76f640a | Alexey Solovyev | 18 September 2019, 05:47:29 UTC | update_database is only loaded in serialization.hl | 18 September 2019, 05:47:29 UTC |
be3ec82 | Alexey Solovyev | 18 September 2019, 00:15:00 UTC | Merge branch 'master' into develop | 18 September 2019, 00:15:00 UTC |
9ab5dec | Alexey Solovyev | 18 September 2019, 00:14:49 UTC | use_serialization.hl | 18 September 2019, 00:14:49 UTC |
adfe470 | Alexey Solovyev | 18 September 2019, 00:13:01 UTC | Added load_flyspeck.ml | 18 September 2019, 00:13:01 UTC |
653e9d1 | Alexey Solovyev | 18 September 2019, 00:11:30 UTC | Removed update_database (and serialization) from strictbuild.hl | 18 September 2019, 00:11:30 UTC |
835e84a | Alexey Solovyev | 07 April 2019, 05:47:52 UTC | Updates | 07 April 2019, 05:47:52 UTC |
11a3b74 | Alexey Solovyev | 13 February 2019, 02:36:55 UTC | Test formatting | 13 February 2019, 02:36:55 UTC |
6a48834 | Alexey Solovyev | 08 February 2019, 03:43:13 UTC | good_list_archive: a faster create_num_list function | 08 February 2019, 03:43:13 UTC |
060adde | Alexey Solovyev | 31 January 2019, 20:19:42 UTC | Removed md5 checks from the_kepler_conjecture.hl: new hash values should be generated | 31 January 2019, 20:19:42 UTC |
b5b75a4 | Alexey Solovyev | 31 January 2019, 01:41:21 UTC | Updated all text_formalization files | 31 January 2019, 01:41:21 UTC |
03663d7 | Alexey Solovyev | 30 January 2019, 08:56:30 UTC | Updated up to tame/tame_def2.hl | 30 January 2019, 08:56:30 UTC |
3ad6700 | Alexey Solovyev | 30 January 2019, 03:48:19 UTC | prime -> prime' in polar_fan.hl | 30 January 2019, 03:48:19 UTC |
17060ce | Alexey Solovyev | 30 January 2019, 02:11:04 UTC | Removed HASH-tactics from counting_spheres.hl | 30 January 2019, 02:11:04 UTC |
da67b8b | Alexey Solovyev | 29 January 2019, 08:00:50 UTC | Removing tactics which depend on hash values of terms | 29 January 2019, 08:00:50 UTC |
920e300 | Alexey Solovyev | 29 January 2019, 08:00:03 UTC | Updated up to Conforming.hl | 29 January 2019, 08:00:03 UTC |
913c9fd | Alexey Solovyev | 29 January 2019, 03:42:32 UTC | .gitattributes | 29 January 2019, 03:42:32 UTC |
fb4ba42 | Alexey Solovyev | 26 January 2019, 02:27:31 UTC | Merge branch 'master' into develop | 26 January 2019, 02:27:31 UTC |
d81fae7 | Alexey Solovyev | 26 January 2019, 02:26:39 UTC | Merge pull request #4 from elimin8r/patch-1 doc(LICENSE): add file documenting license | 26 January 2019, 02:26:39 UTC |
12e081b | Alexey Solovyev | 22 January 2019, 22:18:43 UTC | Updated general/parser_verbose.hl | 22 January 2019, 22:18:43 UTC |
39e8f79 | Alexey Solovyev | 22 January 2019, 18:23:57 UTC | azure: .gitignore + correct camlp5 path | 22 January 2019, 18:23:57 UTC |
04290ce | Joe Pleso | 20 August 2018, 18:55:17 UTC | doc(LICENSE): add file documenting license GitHub community standards recommend committing a license file to avoid any legal ambiguities. | 20 August 2018, 18:55:17 UTC |
c1060e8 | Alexey Solovyev | 01 September 2017, 10:02:03 UTC | or -> ||, & -> && | 01 September 2017, 10:02:03 UTC |
43e4ff7 | Alexey Solovyev | 01 September 2017, 00:32:53 UTC | More formal_ineqs files | 01 September 2017, 00:32:53 UTC |
27f41e1 | Alexey Solovyev | 01 September 2017, 00:29:19 UTC | Updated formal_ineqs | 01 September 2017, 00:29:19 UTC |
c027d71 | Alexey Solovyev | 31 August 2017, 23:59:46 UTC | Renamed some theorems to remove compatibility results | 31 August 2017, 23:59:46 UTC |
f19a2e4 | Alexey Solovyev | 26 August 2017, 05:28:40 UTC | Done (without formal_ineqs) | 26 August 2017, 05:28:40 UTC |
4bdfe27 | Alexey Solovyev | 26 August 2017, 03:42:30 UTC | Done up to local/RNSYJXM-compiled.hl (no lp) | 26 August 2017, 03:42:30 UTC |
2ff2cc4 | Alexey Solovyev | 25 August 2017, 07:34:33 UTC | Done up to local/lp_details.hl (no lp) | 25 August 2017, 07:34:33 UTC |
c1b2594 | Alexey Solovyev | 25 August 2017, 04:11:42 UTC | Done up to packing/OXLZLEZ3.hl | 25 August 2017, 04:11:42 UTC |
3dd4e7a | Alexey Solovyev | 25 August 2017, 02:24:14 UTC | Done up to fan/CFYXFTY.hl | 25 August 2017, 02:24:14 UTC |
5910095 | Alexey Solovyev | 24 August 2017, 08:08:28 UTC | Using the new definition of sqrt (done up to hypermap.hl) | 24 August 2017, 08:08:28 UTC |
015a5d9 | Alexey Solovyev | 03 June 2017, 06:11:58 UTC | Corrected SSReflect/HOL proofs in FNJLBXS.vhl | 03 June 2017, 06:11:58 UTC |
09ebde2 | Alexey Solovyev | 03 June 2017, 06:11:06 UTC | Changed some proofs in add_triangle.vhl to avoid long loadings | 03 June 2017, 06:11:06 UTC |
5aa135c | Alexey Solovyev | 03 June 2017, 06:09:55 UTC | Added .gitignore | 03 June 2017, 06:09:55 UTC |
b37c3d0 | flyspeck | 22 May 2017, 18:21:06 UTC | deleting patch to FNJLBXS.hl (It was fixed by Solovyev) and restoring build.hl | 22 May 2017, 18:21:06 UTC |
c466bc1 | Alexey Solovyev | 22 May 2017, 07:09:16 UTC | FNJLBXS-compiled.hl: new min_k_continuous and min_k_limit proofs | 22 May 2017, 07:09:16 UTC |
1e99ebc | flyspeck | 20 May 2017, 15:21:09 UTC | partial patch of FNJLBXS.hl -build temporarily restricted to early files | 20 May 2017, 15:21:09 UTC |
7eb60c3 | flyspeck | 13 March 2017, 12:47:49 UTC | removed kepler_tex directory, moved to publications project | 13 March 2017, 12:47:49 UTC |
760e932 | flyspeck | 13 March 2017, 12:43:10 UTC | removed usr directoroy | 13 March 2017, 12:43:10 UTC |
152835a | flyspeck | 13 March 2017, 12:38:42 UTC | removed legacy directory | 13 March 2017, 12:38:42 UTC |
f02b253 | flyspeck | 22 February 2017, 17:21:06 UTC | update for accepted version of flyspeck paper | 22 February 2017, 17:21:06 UTC |
392aa53 | Thomas Hales | 17 October 2016, 15:44:03 UTC | changes suggested by referees | 17 October 2016, 15:44:03 UTC |
af5d632 | flyspeck | 10 October 2016, 21:32:42 UTC | added Harrisons parser changes, for OCaml or | 10 October 2016, 21:32:42 UTC |
52c04b7 | flyspeck | 29 April 2016, 21:17:57 UTC | Update README.md | 29 April 2016, 21:17:57 UTC |
c882e47 | flyspeck | 27 April 2016, 21:35:45 UTC | commented out full theorem_digest from serialization.hl | 27 April 2016, 21:35:45 UTC |
3b9efd8 | flyspeck | 02 March 2016, 18:59:34 UTC | Update README.md | 02 March 2016, 18:59:34 UTC |
2a17c50 | flyspeck | 26 February 2016, 15:44:36 UTC | Update README.md | 26 February 2016, 15:44:36 UTC |
3e8dfba | flyspeck | 10 February 2016, 16:30:47 UTC | small update of serialization | 10 February 2016, 16:30:47 UTC |
0db7e5b | flyspeck | 07 February 2016, 20:37:21 UTC | cleaned up serialization | 07 February 2016, 20:37:21 UTC |
4f38636 | flyspeck | 07 February 2016, 17:51:12 UTC | changed IMAGE_DELETE_INJ for HOL Light compatibility | 07 February 2016, 17:51:12 UTC |
b0bb867 | flyspeck | 25 December 2015, 13:43:44 UTC | Updated internal module links in informal_code | 25 December 2015, 13:43:44 UTC |
a2ecf7f | flyspeck | 24 December 2015, 11:26:04 UTC | rearranged files for better separation between informal code and formalization | 24 December 2015, 11:26:04 UTC |
c716272 | flyspeck | 23 December 2015, 04:09:19 UTC | emacs hol-light-mode moved to informal_code/ and updated for emacs 24 | 23 December 2015, 04:09:19 UTC |
b8ceea7 | flyspeck | 19 November 2015, 19:53:37 UTC | force creation of deserialization axiom when loading the_nonlinear_inequalities | 19 November 2015, 19:53:37 UTC |
98185a7 | flyspeck | 07 November 2015, 22:19:14 UTC | corrected build script for the_nonlinear_inequalities | 07 November 2015, 22:19:14 UTC |
7138890 | flyspeck | 06 November 2015, 13:14:39 UTC | Update README.md | 06 November 2015, 13:14:39 UTC |
b88a8f9 | flyspeck | 01 November 2015, 22:49:27 UTC | rechecked texability of tex files | 01 November 2015, 22:49:27 UTC |
2c9b724 | flyspeck | 16 October 2015, 19:22:02 UTC | Update README.md | 16 October 2015, 19:22:02 UTC |
79c329f | flyspeck | 15 October 2015, 19:41:25 UTC | updated github references from google code | 15 October 2015, 19:41:25 UTC |
db1c94b | Alexey | 14 October 2015, 22:42:44 UTC | Hyperlinks in README.md | 14 October 2015, 22:42:44 UTC |
be8bba0 | Alexey | 14 October 2015, 22:37:19 UTC | Hyperlinks in README.md | 14 October 2015, 22:37:19 UTC |
5892ae6 | Alexey | 14 October 2015, 22:25:52 UTC | Hyperlinks in README files | 14 October 2015, 22:25:52 UTC |
5917fd4 | flyspeck | 14 October 2015, 16:00:20 UTC | added downloads README | 14 October 2015, 16:00:20 UTC |
d960853 | flyspeck | 14 October 2015, 15:38:04 UTC | added downloads | 14 October 2015, 15:38:04 UTC |
a2facd6 | flyspeck | 13 October 2015, 18:14:36 UTC | Update README.md | 13 October 2015, 18:14:36 UTC |
042af75 | flyspeck | 13 October 2015, 17:21:08 UTC | Update README.md | 13 October 2015, 17:21:08 UTC |
cf90a76 | flyspeck | 12 October 2015, 21:16:56 UTC | Update README.md | 12 October 2015, 21:16:56 UTC |
6d53941 | flyspeck | 12 October 2015, 21:09:51 UTC | Update README.md | 12 October 2015, 21:09:51 UTC |
d2ba239 | flyspeck | 12 October 2015, 21:08:22 UTC | Update README.md | 12 October 2015, 21:08:22 UTC |
340cc58 | flyspeck | 12 October 2015, 21:03:16 UTC | README changed to markup | 12 October 2015, 21:03:16 UTC |
c832011 | Alexey | 11 October 2015, 21:24:28 UTC | All lp certificates (hard7.dat -> hard7.tar.gz) | 11 October 2015, 21:24:28 UTC |
4a03881 | flyspeck | 10 October 2015, 17:47:27 UTC | The main build script has been updated with corrections suggested by an anonymous referee. | 10 October 2015, 17:47:27 UTC |
eda4c2e | flyspeck | 10 October 2015, 15:08:45 UTC | The primary references to the google svn repository have been removed. | 10 October 2015, 15:08:45 UTC |
ca47bb6 | tchales@gmail.com | 07 May 2015, 18:26:12 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3759 7e6f0243-3638-0410-8646-9b5c9460da73 | 07 May 2015, 18:26:12 UTC |
66154aa | tchales@gmail.com | 07 May 2015, 18:25:54 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3758 7e6f0243-3638-0410-8646-9b5c9460da73 | 07 May 2015, 18:25:54 UTC |
ba9b6e6 | tchales@gmail.com | 03 May 2015, 18:55:33 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3757 7e6f0243-3638-0410-8646-9b5c9460da73 | 03 May 2015, 18:55:33 UTC |
2cee448 | TCHales | 28 April 2015, 21:34:08 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3755 7e6f0243-3638-0410-8646-9b5c9460da73 | 28 April 2015, 21:34:08 UTC |
95ff3b0 | TCHales | 04 April 2015, 19:11:29 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3753 7e6f0243-3638-0410-8646-9b5c9460da73 | 04 April 2015, 19:11:29 UTC |
8bbecd7 | tchales@gmail.com | 04 April 2015, 19:09:54 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3752 7e6f0243-3638-0410-8646-9b5c9460da73 | 04 April 2015, 19:09:54 UTC |
de864db | tchales@gmail.com | 04 April 2015, 15:38:07 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3748 7e6f0243-3638-0410-8646-9b5c9460da73 | 04 April 2015, 15:38:07 UTC |
6a97824 | tchales@gmail.com | 02 April 2015, 13:04:34 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3742 7e6f0243-3638-0410-8646-9b5c9460da73 | 02 April 2015, 13:04:34 UTC |
225963d | TCHales | 01 April 2015, 14:14:18 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3741 7e6f0243-3638-0410-8646-9b5c9460da73 | 01 April 2015, 14:14:18 UTC |
2de587f | TCHales | 31 March 2015, 20:57:57 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3740 7e6f0243-3638-0410-8646-9b5c9460da73 | 31 March 2015, 20:57:57 UTC |
cd0a440 | solovyev.alexey@gmail.com | 31 March 2015, 19:03:02 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3733 7e6f0243-3638-0410-8646-9b5c9460da73 | 31 March 2015, 19:03:02 UTC |
6f67a9b | TCHales | 31 March 2015, 18:49:19 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3731 7e6f0243-3638-0410-8646-9b5c9460da73 | 31 March 2015, 18:49:19 UTC |
11811bb | TCHales | 31 March 2015, 18:46:57 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3730 7e6f0243-3638-0410-8646-9b5c9460da73 | 31 March 2015, 18:46:57 UTC |
c0d0d7e | solovyev.alexey@gmail.com | 31 March 2015, 18:46:29 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3729 7e6f0243-3638-0410-8646-9b5c9460da73 | 31 March 2015, 18:46:29 UTC |
fd7d476 | tchales@gmail.com | 31 March 2015, 00:24:22 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3704 7e6f0243-3638-0410-8646-9b5c9460da73 | 31 March 2015, 00:24:22 UTC |
f493347 | tchales@gmail.com | 30 March 2015, 18:53:42 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3703 7e6f0243-3638-0410-8646-9b5c9460da73 | 30 March 2015, 18:53:42 UTC |
c1279df | tchales@gmail.com | 30 March 2015, 18:30:09 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3702 7e6f0243-3638-0410-8646-9b5c9460da73 | 30 March 2015, 18:30:09 UTC |
70355b5 | tchales@gmail.com | 30 March 2015, 18:16:14 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3701 7e6f0243-3638-0410-8646-9b5c9460da73 | 30 March 2015, 18:16:14 UTC |
9f138b6 | TCHales | 29 March 2015, 19:27:13 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3700 7e6f0243-3638-0410-8646-9b5c9460da73 | 29 March 2015, 19:27:13 UTC |
9c01f86 | TCHales | 28 March 2015, 20:53:23 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3699 7e6f0243-3638-0410-8646-9b5c9460da73 | 28 March 2015, 20:53:23 UTC |
d3eedf0 | TCHales | 28 March 2015, 17:21:51 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3698 7e6f0243-3638-0410-8646-9b5c9460da73 | 28 March 2015, 17:21:51 UTC |
d4b8c0d | TCHales | 20 January 2015, 22:37:26 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3697 7e6f0243-3638-0410-8646-9b5c9460da73 | 20 January 2015, 22:37:26 UTC |
b0938db | TCHales | 20 January 2015, 22:34:07 UTC | git-svn-id: http://flyspeck.googlecode.com/svn/trunk@3696 7e6f0243-3638-0410-8646-9b5c9460da73 | 20 January 2015, 22:34:07 UTC |