| 2015-10-13 |
haftmann |
2015-10-13 |
prod_case as canonical name for product type eliminator
|
file | diff | annotate |
| 2015-10-05 |
blanchet |
2015-10-05 |
avoid unsound simplification of (C (s x)) when s is a selector but not C's
|
file | diff | annotate |
| 2015-09-06 |
haftmann |
2015-09-06 |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file | diff | annotate |
| 2015-08-16 |
wenzelm |
2015-08-16 |
prefer theory_id operations;
tuned signature;
|
file | diff | annotate |
| 2015-06-01 |
haftmann |
2015-06-01 |
separate class for division operator, with particular syntax added in more specific classes
|
file | diff | annotate |
| 2015-04-08 |
wenzelm |
2015-04-08 |
proper context for Object_Logic operations;
|
file | diff | annotate |
| 2015-03-06 |
wenzelm |
2015-03-06 |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file | diff | annotate |
| 2015-03-04 |
wenzelm |
2015-03-04 |
tuned signature -- prefer qualified names;
|
file | diff | annotate |
| 2015-01-24 |
wenzelm |
2015-01-24 |
tuned signature;
|
file | diff | annotate |
| 2014-11-26 |
wenzelm |
2014-11-26 |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file | diff | annotate |
| 2014-11-24 |
blanchet |
2014-11-24 |
no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)
|
file | diff | annotate |
| 2014-10-31 |
wenzelm |
2014-10-31 |
discontinued obsolete Output.urgent_message;
|
file | diff | annotate |
| 2014-10-08 |
wenzelm |
2014-10-08 |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file | diff | annotate |
| 2014-08-19 |
blanchet |
2014-08-19 |
tuning
|
file | diff | annotate |
| 2014-08-16 |
wenzelm |
2014-08-16 |
updated to named_theorems;
|
file | diff | annotate |
| 2014-06-12 |
blanchet |
2014-06-12 |
removed subsumed record-related code, now that records are registered as 'ctr_sugar'
|
file | diff | annotate |
| 2014-06-12 |
blanchet |
2014-06-12 |
made lookup more robust in the face of missing (dummy) case constant
|
file | diff | annotate |
| 2014-03-21 |
wenzelm |
2014-03-21 |
more qualified names;
|
file | diff | annotate |
| 2014-03-21 |
wenzelm |
2014-03-21 |
more qualified names;
|
file | diff | annotate |
| 2014-03-19 |
wenzelm |
2014-03-19 |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
file | diff | annotate |
| 2014-03-15 |
wenzelm |
2014-03-15 |
tuned signature;
eliminated clones;
|
file | diff | annotate |
| 2014-03-03 |
blanchet |
2014-03-03 |
fixed handling of 'case_prod' and other 'case' functions for interpreted types
|
file | diff | annotate |
| 2014-03-03 |
blanchet |
2014-03-03 |
support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
|
file | diff | annotate |
| 2014-03-03 |
blanchet |
2014-03-03 |
tuned ML names
|
file | diff | annotate |
| 2014-03-03 |
blanchet |
2014-03-03 |
tuned code
|
file | diff | annotate |
| 2014-03-03 |
blanchet |
2014-03-03 |
removed nonstandard models from Nitpick
|
file | diff | annotate |
| 2014-03-03 |
blanchet |
2014-03-03 |
guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick
|
file | diff | annotate |
| 2014-02-19 |
blanchet |
2014-02-19 |
adapted Nitpick to 'primrec' refactoring
|
file | diff | annotate |
| 2014-02-17 |
blanchet |
2014-02-17 |
simplified data structure by reducing the incidence of clumsy indices
|
file | diff | annotate |
| 2014-02-12 |
blanchet |
2014-02-12 |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file | diff | annotate |
| 2014-01-20 |
blanchet |
2014-01-20 |
have Nitpick lookup codatatypes
|
file | diff | annotate |
| 2014-01-16 |
blanchet |
2014-01-16 |
adapted to move of Wfrec
|
file | diff | annotate |
| 2013-12-19 |
blanchet |
2013-12-19 |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
file | diff | annotate |
| 2013-11-19 |
haftmann |
2013-11-19 |
eliminiated neg_numeral in favour of - (numeral _)
|
file | diff | annotate |
| 2013-11-10 |
haftmann |
2013-11-10 |
dropped obsolete check: dest_num always yields positive number
|
file | diff | annotate |
| 2013-09-24 |
blanchet |
2013-09-24 |
encode goal digest in spying log (to detect duplicates)
|
file | diff | annotate |
| 2013-09-23 |
blanchet |
2013-09-23 |
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
|
file | diff | annotate |
| 2013-05-28 |
blanchet |
2013-05-28 |
don't create needless constant
|
file | diff | annotate |
| 2013-04-15 |
blanchet |
2013-04-15 |
not all Nitpick 'constructors' are injective -- careful
|
file | diff | annotate |
| 2013-02-15 |
haftmann |
2013-02-15 |
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
|
file | diff | annotate |
| 2012-10-31 |
blanchet |
2012-10-31 |
moved Refute to "HOL/Library" to speed up building "Main" even more
|
file | diff | annotate |
| 2012-10-12 |
wenzelm |
2012-10-12 |
discontinued typedef with implicit set_def;
|
file | diff | annotate |
| 2012-08-15 |
blanchet |
2012-08-15 |
fixed handling of "int" in the wake of its port to the quotient package
|
file | diff | annotate |
| 2012-08-15 |
blanchet |
2012-08-15 |
removed dead code
|
file | diff | annotate |
| 2012-05-24 |
blanchet |
2012-05-24 |
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 |
| 2012-05-11 |
blanchet |
2012-05-11 |
fixed "real" after they were redefined as a 'quotient_type'
|
file | diff | annotate |
| 2012-04-26 |
blanchet |
2012-04-26 |
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 |
| 2012-04-22 |
blanchet |
2012-04-22 |
more meaningful default value
|
file | diff | annotate |
| 2012-04-22 |
blanchet |
2012-04-22 |
handle exception (needed to solve TPTP problem SEU880^5)
|
file | diff | annotate |
| 2012-04-03 |
griff |
2012-04-03 |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file | diff | annotate |
| 2012-03-26 |
blanchet |
2012-03-26 |
fixed Nitpick after numeral representation change (2a1953f0d20d)
|
file | diff | annotate |
| 2012-03-25 |
huffman |
2012-03-25 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| 2012-03-04 |
blanchet |
2012-03-04 |
addressed a quotient-type-related issue that arose with the port to "set"
|
file | diff | annotate |
| 2012-03-01 |
blanchet |
2012-03-01 |
improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case
|
file | diff | annotate |
| 2012-03-01 |
blanchet |
2012-03-01 |
fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction
|
file | diff | annotate |
| 2012-01-23 |
blanchet |
2012-01-23 |
renamed two files to make room for a new file
|
file | diff | annotate |
| 2012-01-17 |
blanchet |
2012-01-17 |
fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick
|
file | diff | annotate |
| 2012-01-14 |
wenzelm |
2012-01-14 |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file | diff | annotate |
| 2012-01-14 |
wenzelm |
2012-01-14 |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file | diff | annotate |
| 2012-01-04 |
blanchet |
2012-01-04 |
improved "set" support by code inspection
|
file | diff | annotate |