| Sat, 01 Feb 2014 18:05:03 +0100 | wenzelm | proper Simplifier method setup; | changeset | files |
| Sat, 01 Feb 2014 18:00:28 +0100 | wenzelm | simplified sessions; | changeset | files |
| Sat, 01 Feb 2014 17:56:03 +0100 | wenzelm | misc tuning and modernization; | changeset | files |
| Sat, 01 Feb 2014 00:32:32 +0000 | paulson | version of Fermat's Theorem for type nat | changeset | files |
| Fri, 31 Jan 2014 19:32:13 +0100 | wenzelm | merged | changeset | files |
| Fri, 31 Jan 2014 18:58:50 +0100 | wenzelm | merged | changeset | files |
| Fri, 31 Jan 2014 17:35:19 +0100 | wenzelm | include comment.sty 3.6 which still works with plain tex, in contrast to later 3.7 which is only for latex (slow due to file snippets) -- see also 30781cc78fc6; | changeset | files |
| Fri, 31 Jan 2014 19:16:41 +0100 | blanchet | generalized preplaying infrastructure to store various results for various methods | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | added a 'trace' option | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | tuning | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | moved code around | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | added 'algebra' to the mix | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | more informative trace | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | tuning | changeset | files |
| Fri, 31 Jan 2014 18:43:16 +0100 | blanchet | more concise Isar output | changeset | files |
| Fri, 31 Jan 2014 16:58:58 +0000 | paulson | Restoring some proofs from the equivalent file in Old_Number_Theory. | changeset | files |
| Fri, 31 Jan 2014 16:41:54 +0100 | blanchet | better tracing + syntactically correct 'metis' calls | changeset | files |
| Fri, 31 Jan 2014 16:26:43 +0100 | blanchet | tuned ML function names | changeset | files |
| Fri, 31 Jan 2014 16:10:39 +0100 | blanchet | tuning | changeset | files |
| Fri, 31 Jan 2014 16:07:20 +0100 | blanchet | moved ML code around | changeset | files |
| Fri, 31 Jan 2014 14:33:02 +0100 | wenzelm | tuned headers; | changeset | files |
| Fri, 31 Jan 2014 13:45:39 +0100 | blanchet | merge | changeset | files |
| Fri, 31 Jan 2014 13:42:47 +0100 | blanchet | compile | changeset | files |
| Fri, 31 Jan 2014 13:32:13 +0100 | blanchet | guarded against exception | changeset | files |
| Fri, 31 Jan 2014 13:29:20 +0100 | blanchet | tuning | changeset | files |
| Fri, 31 Jan 2014 12:30:54 +0100 | blanchet | refactor large ML file | changeset | files |
| Fri, 31 Jan 2014 12:16:59 +0100 | traytel | use Local_Theory.define instead of Specification.definition for internal constants | changeset | files |
| Fri, 31 Jan 2014 10:34:20 +0100 | blanchet | compile | changeset | files |
| Fri, 31 Jan 2014 10:23:32 +0100 | blanchet | renamed many Sledgehammer ML files to clarify structure | changeset | files |
| Fri, 31 Jan 2014 10:23:32 +0100 | blanchet | renamed ML file | changeset | files |