src/HOL/Tools/Nitpick/HISTORY
author blanchet
Thu, 05 Nov 2009 19:06:35 +0100
changeset 33581 e1e77265fb1d
parent 33565 5fad8e36dfb1
child 33582 bdf98e327f0b
permissions -rw-r--r--
added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     1
Version 2010
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     2
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     3
  * Moved into Isabelle/HOL "Main"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     4
  * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     5
    "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     6
    "nitpick_ind_intro" to "nitpick_intro"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     7
  * Replaced "special_depth" and "skolemize_depth" options by "specialize"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
     8
    and "skolemize"
33556
cba22e2999d5 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents: 33197
diff changeset
     9
  * Renamed "coalesce_type_vars" to "merge_type_vars"
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
    10
  * Optimized Kodkod encoding of datatypes whose constructors don't appear in
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33556
diff changeset
    11
    the formula to falsify
33581
e1e77265fb1d added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents: 33565
diff changeset
    12
  * Added support for codatatype view of datatypes
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    13
  * Fixed monotonicity check
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
    14
  * Fixed error in display of uncurried constants
33581
e1e77265fb1d added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents: 33565
diff changeset
    15
  * Speeded up scope enumeration
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    16
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    17
Version 1.2.2 (16 Oct 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    18
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    19
  * Added and implemented "star_linear_preds" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    20
  * Added and implemented "format" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    21
  * Added and implemented "coalesce_type_vars" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    22
  * Added and implemented "max_genuine" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    23
  * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    24
    "-1::nat", subset, constructors, sort axioms, and partially applied
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    25
    interpreted constants
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    26
  * Fixed error in "show_consts" for boxed specialized constants
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    27
  * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    28
  * Fixed display of Skolem constants
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    29
  * Fixed error in "check_potential" and "check_genuine"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    30
  * Added boxing support for higher-order constructor parameters
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    31
  * Changed notation used for coinductive datatypes
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    32
  * Optimized Kodkod encoding of "If", "card", and "setsum"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    33
  * Improved the monotonicity check
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    34
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    35
Version 1.2.1 (25 Sep 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    36
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    37
  * Added explicit support for coinductive datatypes
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    38
  * Added and implemented "box" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    39
  * Added and implemented "fast_descrs" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    40
  * Added and implemented "uncurry" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    41
  * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    42
  * Fixed soundness issue related to nullary constructors
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    43
  * Fixed soundness issue related to higher-order quantifiers
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    44
  * Fixed soundness issue related to the "destroy_constrs" optimization
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    45
  * Fixed soundness issues related to the "special_depth" optimization
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    46
  * Added support for PicoSAT and incorporated it with the Nitpick package
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    47
  * Added automatic detection of installed SAT solvers based on naming
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    48
    convention
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    49
  * Optimized handling of quantifiers by moving them inward whenever possible
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    50
  * Optimized and improved precision of "wf" and "wfrec"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    51
  * Improved handling of definitions made in locales
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    52
  * Fixed checked scope count in message shown upon interruption and timeout
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    53
  * Added minimalistic Nitpick-like tool called Minipick
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    54
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    55
Version 1.2.0 (27 Jul 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    56
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    57
  * Optimized Kodkod encoding of datatypes and records
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    58
  * Optimized coinductive definitions
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    59
  * Fixed soundness issues related to pairs of functions
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    60
  * Fixed soundness issue in the peephole optimizer
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    61
  * Improved precision of non-well-founded predicates occurring positively in
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    62
    the formula to falsify
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    63
  * Added and implemented "destroy_constrs" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    64
  * Changed semantics of "inductive_mood" option to ensure soundness
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    65
  * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    66
    "sync_cards"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    67
  * Improved precision of "trancl" and "rtrancl"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    68
  * Optimized Kodkod encoding of "tranclp" and "rtranclp"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    69
  * Made detection of inconsistent scope specifications more robust
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    70
  * Fixed a few Kodkod generation bugs that resulted in exceptions
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    71
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    72
Version 1.1.1 (24 Jun 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    73
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    74
  * Added "show_all" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    75
  * Fixed soundness issues related to type classes
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    76
  * Improved precision of some set constructs
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    77
  * Fiddled with the automatic monotonicity check
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    78
  * Fixed performance issues related to scope enumeration
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    79
  * Fixed a few Kodkod generation bugs that resulted in exceptions or stack
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    80
    overflows
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    81
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    82
Version 1.1.0 (16 Jun 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    83
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    84
  * Redesigned handling of datatypes to provide an interface baded on "card" and
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    85
    "max", obsoleting "mult"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    86
  * Redesigned handling of typedefs, "rat", and "real"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    87
  * Made "lockstep" option a three-state option and added an automatic
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    88
    monotonicity check
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    89
  * Made "batch_size" a (n + 1)-state option whose default depends on whether
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    90
    "debug" is enabled
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    91
  * Made "debug" automatically enable "verbose"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    92
  * Added "destroy_equals" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    93
  * Added "no_assms" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    94
  * Fixed bug in computation of ground type 
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    95
  * Fixed performance issue related to datatype acyclicity constraint generation
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    96
  * Fixed performance issue related to axiom selection
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    97
  * Improved precision of some well-founded inductive predicates
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    98
  * Added more checks to guard against very large cardinalities
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
    99
  * Improved hit rate of potential counterexamples
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   100
  * Fixed several soundness issues
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   101
  * Optimized the Kodkod encoding to benefit more from symmetry breaking
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   102
  * Optimized relational composition, cartesian product, and converse
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   103
  * Added support for HaifaSat
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   104
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   105
Version 1.0.3 (17 Mar 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   106
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   107
  * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   108
  * Added "overlord" option to assist debugging
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   109
  * Increased default value of "special_depth" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   110
  * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   111
  * Ensured that no scopes are skipped when multithreading is enabled
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   112
  * Fixed soundness issue in handling of "The", "Eps", and partial functions
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   113
    defined using Isabelle's function package
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   114
  * Fixed soundness issue in handling of non-definitional axioms
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   115
  * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   116
    "nat", "int", and "*"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   117
  * Fixed a few Kodkod generation bugs that resulted in exceptions
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   118
  * Optimized "div", "mod", and "dvd" on "nat" and "int"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   119
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   120
Version 1.0.2 (12 Mar 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   121
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   122
  * Added support for non-definitional axioms
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   123
  * Improved Isar integration
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   124
  * Added support for multiplicities of 0
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   125
  * Added "max_threads" option and support for multithreaded Kodkodi
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   126
  * Added "blocking" option to control whether Nitpick should be run
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   127
    synchronously or asynchronously
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   128
  * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   129
  * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   130
  * Introduced "auto_timeout" to specify Auto Nitpick's time limit
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   131
  * Renamed the possible values for the "expect" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   132
  * Renamed the "peephole" option to "peephole_optim"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   133
  * Added negative versions of all Boolean options and made "= true" optional
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   134
  * Altered order of automatic SAT solver selection
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   135
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   136
Version 1.0.1 (6 Mar 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   137
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   138
  * Eliminated the need to import "Nitpick" to use "nitpick"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   139
  * Added "debug" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   140
  * Replaced "specialize_funs" with the more general "special_depth" option
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   141
  * Renamed "watch" option to "eval"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   142
  * Improved parsing of "card", "mult", and "iter" options
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   143
  * Fixed a soundness bug in the "specialize_funs" optimization
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   144
  * Increased the scope of the "specialize_funs" optimization
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   145
  * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   146
  * Fixed a soundness bug in the "subterm property" optimization for types of
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   147
    cardinality 1
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   148
  * Improved the axiom selection for overloaded constants, which led to an
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   149
    infinite loop for "Nominal.perm"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   150
  * Added support for multiple instantiations of non-well-founded inductive
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   151
    predicates, which previously raised an exception
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   152
  * Fixed a Kodkod generation bug that resulted in an exception
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   153
  * Altered order of scope enumeration and automatic SAT solver selection
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   154
  * Optimized "Eps", "nat_case", and "list_case"
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   155
  * Improved output formatting
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   156
  * Added checks to prevent infinite loops in axiom selector and constant
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   157
    unfolding
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   158
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   159
Version 1.0.0 (27 Feb 2009)
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   160
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset
   161
  * First release