src/HOL/Tools/refute_isar.ML
2010-09-02 wenzelm 2010-09-02 just one refute.ML;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2009-12-14 blanchet 2009-12-14 added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections
2009-10-28 wenzelm 2009-10-28 back to Proof.raw_goal;
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-10-02 wenzelm 2009-10-02 misc tuning and simplification;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-01-28 wenzelm 2008-01-28 removed redundant repeatd scanner combinator;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-01-19 webertj 2007-01-19 reformatted to 80 chars/line
2005-09-06 webertj 2005-09-06 unnecessary parentheses removed
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-03-10 webertj 2004-03-10 *** empty log message ***
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.