Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_isar.ML
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code file | diff | annotate
Thu, 21 Nov 2013 12:29:29 +0100 blanchet fixed spying so that the envirnoment variables are queried at run-time not at build-time file | diff | annotate
Mon, 23 Sep 2013 14:53:43 +0200 blanchet added "spy" option to Nitpick file | diff | annotate
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function); file | diff | annotate
Fri, 12 Jul 2013 23:45:05 +0200 wenzelm system options for Isabelle/HOL proof tools; file | diff | annotate
Wed, 15 May 2013 22:30:24 +0200 wenzelm clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x; file | diff | annotate
Wed, 15 May 2013 20:22:46 +0200 wenzelm maintain ProofGeneral preferences within ProofGeneral module; file | diff | annotate
Wed, 15 May 2013 17:39:41 +0200 wenzelm just one ProofGeneral module; file | diff | annotate
Sat, 11 May 2013 16:57:18 +0200 wenzelm prefer explicitly qualified exceptions, which is particular important for robust handlers; file | diff | annotate
Wed, 27 Mar 2013 17:58:07 +0100 wenzelm more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs); file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved Refute to "HOL/Library" to speed up building "Main" even more file | diff | annotate
Thu, 27 Sep 2012 17:00:54 +0200 blanchet lower the defaults for the number of bits, based on an example by Lukas Bulwahn file | diff | annotate
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations; file | diff | annotate
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser; file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet unbreak "max_potential" logic file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet handle non-auto try case gracefully in Nitpick file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "Auto_Tools" "Try" file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet use \<emdash> rather than \<midarrow> file | diff | annotate
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Thu, 17 Mar 2011 22:07:17 +0100 blanchet reintroduced "show_skolems" option -- useful when too many Skolems are displayed file | diff | annotate
Thu, 03 Mar 2011 11:20:48 +0100 blanchet simplify "need" option's syntax file | diff | annotate
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need" file | diff | annotate
Mon, 28 Feb 2011 17:53:10 +0100 blanchet added "total_consts" option file | diff | annotate
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct") file | diff | annotate
Mon, 21 Feb 2011 15:45:44 +0100 blanchet first steps in implementing "fix_datatype_vals" optimization file | diff | annotate
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage; file | diff | annotate
Fri, 03 Dec 2010 09:55:45 +0100 blanchet run synchronous Auto Tools in parallel file | diff | annotate
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts file | diff | annotate
Tue, 14 Sep 2010 13:24:18 +0200 blanchet remove "fast_descs" option from Nitpick; file | diff | annotate
Mon, 13 Sep 2010 20:27:40 +0200 blanchet remove "atoms" from the list of options with default values file | diff | annotate
Mon, 13 Sep 2010 20:21:24 +0200 blanchet make Auto Nitpick go through fewer scopes file | diff | annotate
Sat, 11 Sep 2010 12:31:58 +0200 blanchet tuning file | diff | annotate
Sat, 11 Sep 2010 10:35:00 +0200 blanchet finished renaming "Auto_Counterexample" to "Auto_Tools" file | diff | annotate
Sat, 11 Sep 2010 10:20:25 +0200 blanchet change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads) file | diff | annotate
Mon, 06 Sep 2010 13:06:27 +0200 wenzelm some results of concurrency code inspection; file | diff | annotate
Wed, 01 Sep 2010 21:47:25 +0200 blanchet more elegant ML file | diff | annotate
Thu, 05 Aug 2010 20:17:50 +0200 blanchet added "whack" file | diff | annotate
Tue, 03 Aug 2010 14:49:42 +0200 blanchet bump up the max cardinalities, to use up more of the time given to us by the user file | diff | annotate
Sun, 01 Aug 2010 16:35:25 +0200 blanchet tweak datatype sym break code file | diff | annotate
Sat, 31 Jul 2010 16:39:32 +0200 blanchet started implementation of custom sym break file | diff | annotate
Tue, 01 Jun 2010 12:20:08 +0200 blanchet added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML" file | diff | annotate
Mon, 31 May 2010 17:20:41 +0200 blanchet fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option file | diff | annotate
Thu, 27 May 2010 16:42:03 +0200 blanchet make Nitpick "show_all" option behave less surprisingly file | diff | annotate
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; file | diff | annotate
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing; file | diff | annotate
Sat, 01 May 2010 21:29:03 +0200 krauss made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224) file | diff | annotate
Sun, 25 Apr 2010 00:33:26 +0200 blanchet cosmetics file | diff | annotate
Sun, 25 Apr 2010 00:25:44 +0200 blanchet remove "show_skolems" option and change style of record declarations file | diff | annotate
Sun, 25 Apr 2010 00:10:30 +0200 blanchet remove "skolemize" option from Nitpick, since Skolemization is always useful file | diff | annotate
Sat, 24 Apr 2010 17:48:21 +0200 blanchet removed Nitpick's "uncurry" option file | diff | annotate
Sat, 24 Apr 2010 16:43:03 +0200 blanchet Fruhjahrsputz: remove three mostly useless Nitpick options file | diff | annotate
Sat, 24 Apr 2010 16:33:01 +0200 blanchet remove type annotations as comments; file | diff | annotate
Fri, 23 Apr 2010 19:18:39 +0200 blanchet stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name file | diff | annotate
Wed, 24 Mar 2010 14:43:35 +0100 blanchet simplify Nitpick parameter parsing code a little bit + make compile file | diff | annotate
Tue, 23 Mar 2010 11:40:46 +0100 blanchet leverage code now in Sledgehammer file | diff | annotate
Fri, 19 Mar 2010 15:07:44 +0100 blanchet move the Sledgehammer Isar commands together into one file; file | diff | annotate
Tue, 09 Mar 2010 09:25:23 +0100 blanchet added "finitize" option to Nitpick + remove dependency on "Coinductive_List" file | diff | annotate
Mon, 22 Feb 2010 11:57:33 +0100 blanchet fixed a few bugs in Nitpick and removed unreferenced variables file | diff | annotate
less more (0) -60 tip
isabelle