| Wed, 19 Feb 2014 08:34:34 +0100 |
blanchet |
adapted Nitpick to 'primrec' refactoring
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 22:54:38 +0100 |
blanchet |
simplified data structure by reducing the incidence of clumsy indices
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 19:51:56 +0100 |
blanchet |
have Nitpick lookup codatatypes
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 16:20:17 +0100 |
blanchet |
adapted to move of Wfrec
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 13:43:21 +0100 |
blanchet |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 10:02:34 +0100 |
haftmann |
dropped obsolete check: dest_num always yields positive number
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 11:02:42 +0200 |
blanchet |
encode goal digest in spying log (to detect duplicates)
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 18:40:02 +0200 |
blanchet |
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
|
file |
diff |
annotate
|
| Tue, 28 May 2013 19:59:54 +0200 |
blanchet |
don't create needless constant
|
file |
diff |
annotate
|
| Mon, 15 Apr 2013 10:41:03 +0200 |
blanchet |
not all Nitpick 'constructors' are injective -- careful
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
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
|
| Fri, 12 Oct 2012 15:08:29 +0200 |
wenzelm |
discontinued typedef with implicit set_def;
|
file |
diff |
annotate
|
| Wed, 15 Aug 2012 11:04:56 +0200 |
blanchet |
fixed handling of "int" in the wake of its port to the quotient package
|
file |
diff |
annotate
|
| Wed, 15 Aug 2012 11:04:55 +0200 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Thu, 24 May 2012 17:46:35 +0200 |
blanchet |
fixed soundness bug in Nitpick related to unfolding -- the unfolding criterion must at least as strict when looking at a definitional axiom as elsewhere, otherwise we end up unfolding a constant's definition in its own definition, yielding a trivial equality
|
file |
diff |
annotate
|
| Fri, 11 May 2012 00:45:24 +0200 |
blanchet |
fixed "real" after they were redefined as a 'quotient_type'
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 20:09:38 +0200 |
blanchet |
fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
more meaningful default value
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:45 +0200 |
blanchet |
handle exception (needed to solve TPTP problem SEU880^5)
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:26:30 +0900 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 10:42:06 +0200 |
blanchet |
fixed Nitpick after numeral representation change (2a1953f0d20d)
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 23:20:43 +0100 |
blanchet |
addressed a quotient-type-related issue that arose with the port to "set"
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 11:28:56 +0100 |
blanchet |
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 11:28:56 +0100 |
blanchet |
fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 18:25:36 +0100 |
blanchet |
fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2012 12:09:53 +0100 |
blanchet |
improved "set" support by code inspection
|
file |
diff |
annotate
|
| Wed, 04 Jan 2012 12:09:53 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 23:41:59 +0100 |
blanchet |
fixed bisimilarity axiom -- avoid "insert" with wrong type
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
more robust destruction of "set Collect" idiom
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
handle starred predicates correctly w.r.t. "set"
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
simplify mem Collect
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
fixed set extensionality code
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
construct correct "set" type for wf goal
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
fixed Nitpick's typedef handling w.r.t. "set"
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
rationalized output (a bit)
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
port part of Nitpick to "set" type constructor
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
ported mono calculus to handle "set" type constructors
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 16:14:58 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 14:14:37 +0100 |
kuncar |
make ctxt the first parameter
|
file |
diff |
annotate
|
| Thu, 27 Oct 2011 21:02:10 +0200 |
wenzelm |
localized quotient data;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2011 20:26:38 +0200 |
wenzelm |
simplified/standardized signatures;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2011 13:50:54 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 13:07:00 +0200 |
krauss |
updated unchecked forward reference
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 12:27:24 +0200 |
krauss |
replaced Nitpick's hardwired basic_ersatz_table by context data
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:03:14 +0200 |
krauss |
added dynamic ersatz_table to Nitpick's data slot
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
fixed de Bruijn index bug
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 05 May 2011 12:40:48 +0200 |
blanchet |
query typedefs as well for monotonicity
|
file |
diff |
annotate
|
| Wed, 04 May 2011 19:35:48 +0200 |
blanchet |
exploit inferred monotonicity
|
file |
diff |
annotate
|