Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
Mon, 28 Mar 2016 12:11:54 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
Thu, 06 Nov 2014 15:05:15 +0100 |
wenzelm |
prefer explicit Keyword.keywords (cf. 82a71046dce8);
|
file |
diff |
annotate
|
Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
added options to Mirabelle
|
file |
diff |
annotate
|
Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
file |
diff |
annotate
|
Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 14:19:43 +0200 |
blanchet |
renamed 'sh_minimize' to 'minimize'; compile;
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed 'metisFT' support in Mirabelle
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed Mirabelle minimization code
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
modernized Mirabelle (a bit) and made it compile
|
file |
diff |
annotate
|
Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
Thu, 01 May 2014 09:30:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
Fri, 04 Apr 2014 19:09:56 +0200 |
blanchet |
added option to Mirabelle
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 15:19:07 +0100 |
blanchet |
merged 'reconstructors' and 'proof methods'
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 16:07:20 +0100 |
blanchet |
moved ML code around
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 13:42:47 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
|
Thu, 19 Dec 2013 17:52:58 +0100 |
blanchet |
refactored preplaying outcome data structure
|
file |
diff |
annotate
|
Thu, 19 Dec 2013 09:28:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 18:34:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 17:37:35 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 20:49:19 +0200 |
blanchet |
generate a comment storing the goal nickname in "learn_prover"
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 02:22:54 +0200 |
blanchet |
thread the goal through instead of relying on unreliable (possibly fake) state
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 01:22:15 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 01:10:08 +0200 |
blanchet |
if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
|
file |
diff |
annotate
|
Mon, 19 Aug 2013 12:05:33 +0200 |
blanchet |
improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
|
file |
diff |
annotate
|
Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|
Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:49:18 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Sun, 12 May 2013 20:46:17 +0200 |
wenzelm |
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 17:15:06 +0100 |
blanchet |
tweaked hack some more
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 15:43:51 +0100 |
blanchet |
improved hack
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 14:47:19 +0100 |
blanchet |
trust preplayed proof in Mirabelle
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 17:01:06 +0100 |
blanchet |
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
file |
diff |
annotate
|
Sun, 13 Jan 2013 22:00:45 +0100 |
blanchet |
more informative output
|
file |
diff |
annotate
|