isabelle: File revisions

src/HOL/Tools/refute_isar.ML

2010-09-02	wenzelm	2010-09-02	just one refute.ML;	file \| diff \| annotate
2010-05-17	wenzelm	2010-05-17	prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;	file \| diff \| annotate
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	file \| diff \| annotate
2009-10-28	wenzelm	2009-10-28	back to Proof.raw_goal;	file \| diff \| annotate
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;	file \| diff \| annotate
2009-10-02	wenzelm	2009-10-02	misc tuning and simplification;	file \| diff \| annotate
2008-05-17	wenzelm	2008-05-17	cat_lines;	file \| diff \| annotate
2008-01-28	wenzelm	2008-01-28	removed redundant repeatd scanner combinator;	file \| diff \| annotate
2007-10-06	wenzelm	2007-10-06	simplified interfaces for outer syntax;	file \| diff \| annotate
2007-01-19	webertj	2007-01-19	reformatted to 80 chars/line	file \| diff \| annotate
2005-09-06	webertj	2005-09-06	unnecessary parentheses removed	file \| diff \| annotate
2005-08-16	wenzelm	2005-08-16	OuterKeyword;	file \| diff \| annotate
2005-03-03	skalberg	2005-03-03	Move towards standard functions.	file \| diff \| annotate
2004-03-10	webertj	2004-03-10	* empty log message *	file \| diff \| annotate
2004-01-10	webertj	2004-01-10	Adding 'refute' to HOL.	file \| diff \| annotate

isabelle

RSS Atom