2009-10-02 wenzelm 2009-10-02 Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics); command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-21 haftmann 2009-06-21 simplified names of common datatype types
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-11 haftmann 2009-03-11 HOLogic.mk_set, HOLogic.dest_set
2009-03-07 blanchet 2009-03-07 Added a second timeout mechanism to Refute. For some reason, TimeLimit.timeLimit often does not work, and it leaves Refute running forever, making any evaluation using Mutabelle or Mirabelle impossible. The redundant timeout seems to do the trick.
2009-03-07 blanchet 2009-03-07 Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
2009-03-06 blanchet 2009-03-06 Added "expect" option to Refute, like in Nitpick, that allows to write regression tests. Also replaced calls to "Output.immediate_output" with "priority" or "tracing", because "immediate_output" causes some problems (as explained by Makarius to Sascha).
2009-03-06 blanchet 2009-03-06 Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead. I tested the affected symbols (card, finite, lfp, and gfp), and Refute now works better than before (i.e., more precision and more speed).
2009-03-06 haftmann 2009-03-06 merged
2009-03-05 haftmann 2009-03-05 merged
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05 blanchet 2009-03-05 Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Made Refute.norm_rhs public, so I can use it in Nitpick.
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-17 blanchet 2009-02-17 Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
2009-02-06 blanchet 2009-02-06 Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
2009-02-04 blanchet 2009-02-04 Make some Refute functions public so I can use them in Nitpick, use @{const_name} antiquotation whenever possible (some, like Lfp.lfp had been renamed since Tjark wrote Refute), and removed some "set"-related code that is no longer relevant in Isabelle2008. There's still some "set" code that needs to be ported; see TODO in the file.
2009-01-01 wenzelm 2009-01-01 avoid polymorphic equality;
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2007-12-05 haftmann 2007-12-05 map_product and fold_product
2007-10-15 webertj 2007-10-15 interpreter for List.append added again
2007-10-12 webertj 2007-10-12 significant code overhaul, bugfix for inductive data types
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again);
2007-09-24 wenzelm 2007-09-24 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 cleaned-up Output functions;
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-01-19 webertj 2007-01-19 interpreter for Finite_Set.finite added
2007-01-19 webertj 2007-01-19 reformatted to 80 chars/line
2007-01-10 webertj 2007-01-10 tuned
2007-01-05 webertj 2007-01-05 reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)
2007-01-04 webertj 2007-01-04 using Array.modifyi (no functional change)
2007-01-04 webertj 2007-01-04 obsolete sign_of calls removed
2007-01-04 webertj 2007-01-04 constants are unfolded, universal quantifiers are stripped, some minor changes
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-11-27 webertj 2006-11-27 outermost universal quantifiers are stripped
2006-11-09 webertj 2006-11-09 interpreters for fst and snd added
2006-10-23 haftmann 2006-10-23 switched merge_alists'' to AList.merge'' whenever appropriate
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-20 haftmann 2006-10-20 Symtab.foldl replaced by Symtab.fold
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-15 webertj 2006-09-15 trivial whitespace change
2006-07-11 wenzelm 2006-07-11 removed obsolete mem_term;