2014-02-02 blanchet 2014-02-02 'primitive' is not an adverb
2014-02-02 blanchet 2014-02-02 unform treatment of preplay_timeout = 0 and > 0
2014-02-02 blanchet 2014-02-02 refactor data structure (step 1)
2014-02-02 blanchet 2014-02-02 tuned code
2014-02-02 blanchet 2014-02-02 tuned factor
2014-02-02 blanchet 2014-02-02 tuning
2014-02-02 blanchet 2014-02-02 made SML/NJ happier
2014-02-02 blanchet 2014-02-02 take intersection rather than union of methods when merging steps -- more efficient and natural
2014-02-02 blanchet 2014-02-02 merge proof methods
2014-02-02 blanchet 2014-02-02 use Skolem proof methods appropriately
2014-02-02 blanchet 2014-02-02 simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
2014-02-02 blanchet 2014-02-02 reset timing information after changes
2014-02-02 paulson 2014-02-02 Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
2014-02-01 wenzelm 2014-02-01 merged
2014-02-01 wenzelm 2014-02-01 proper config options; proper context for printing;
2014-02-01 wenzelm 2014-02-01 more standard file/module names;
2014-02-01 paulson 2014-02-01 Added material from Old_Number_Theory related to the Chinese Remainder Theorem
2014-02-01 wenzelm 2014-02-01 prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
2014-02-01 wenzelm 2014-02-01 proper context for printing;
2014-02-01 wenzelm 2014-02-01 more explicit low-level exception;
2014-02-01 wenzelm 2014-02-01 unused;
2014-02-01 wenzelm 2014-02-01 method_setup "lem";
2014-02-01 wenzelm 2014-02-01 lazy_pack is default context for ILL;
2014-02-01 wenzelm 2014-02-01 unused;
2014-02-01 wenzelm 2014-02-01 proper Simplifier method setup;
2014-02-01 wenzelm 2014-02-01 simplified sessions;
2014-02-01 wenzelm 2014-02-01 misc tuning and modernization;
2014-02-01 paulson 2014-02-01 version of Fermat's Theorem for type nat
2014-01-31 wenzelm 2014-01-31 merged
2014-01-31 wenzelm 2014-01-31 merged
2014-01-31 wenzelm 2014-01-31 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;
2014-01-31 blanchet 2014-01-31 generalized preplaying infrastructure to store various results for various methods
2014-01-31 blanchet 2014-01-31 added a 'trace' option
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 moved code around
2014-01-31 blanchet 2014-01-31 added 'algebra' to the mix
2014-01-31 blanchet 2014-01-31 more informative trace
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 more concise Isar output
2014-01-31 paulson 2014-01-31 Restoring some proofs from the equivalent file in Old_Number_Theory.
2014-01-31 blanchet 2014-01-31 better tracing + syntactically correct 'metis' calls
2014-01-31 blanchet 2014-01-31 tuned ML function names
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 moved ML code around
2014-01-31 wenzelm 2014-01-31 tuned headers;
2014-01-31 blanchet 2014-01-31 merge
2014-01-31 blanchet 2014-01-31 compile
2014-01-31 blanchet 2014-01-31 guarded against exception
2014-01-31 blanchet 2014-01-31 tuning
2014-01-31 blanchet 2014-01-31 refactor large ML file
2014-01-31 traytel 2014-01-31 use Local_Theory.define instead of Specification.definition for internal constants
2014-01-31 blanchet 2014-01-31 compile
2014-01-31 blanchet 2014-01-31 renamed many Sledgehammer ML files to clarify structure
2014-01-31 blanchet 2014-01-31 renamed ML file
2014-01-31 blanchet 2014-01-31 tuned comment
2014-01-31 blanchet 2014-01-31 tuned ML file name
2014-01-31 blanchet 2014-01-31 tuned ML file name
2014-01-31 traytel 2014-01-31 less hermetic tactics
2014-01-30 blanchet 2014-01-30 merged
2014-01-30 blanchet 2014-01-30 reverted unsound optimization