an executable version of accessible part (only for finite types yet)

adding yet another induction rule on natural numbers

moving declarations back to the section they seem to belong to (cf. afffe1f72143)

reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code

adding some more examples for quickcheck; replaced FIXME comments

new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well

removed duplicate definitions that made locale inconsistent

added parity analysis

corrected expectation; added an example for quickcheck

adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck

made SML/NJ happy

even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant

separate orthogonal components

generate left-to-right rewrite tag for combinator helpers for SPASS 3.8

better handling of individual type for DFG format (SPASS)

adding quickcheck example with THE

evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.

using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4

tuned

adding very basic code generation to Wellfounded theory

removing dead code from Mutabelle; tuned

generalizing check if size matters because it is different for random and exhaustive testing

merged

adding code equation for Collect on finite types

Use lookup_size rather than Datatype.get_info in is_poly to avoid incorrect results for datatypes on which no size function is defined

adding some rules to quickcheck's preprocessing

some more constants on mutabelle's blacklist

implemented "tptp_refute" tool

added problem importer

imported patch ATP_Problem_Import.thy

imported patch atp_problem_import.ML

renamed theory exporter

renamed two files to make room for a new file

rebranded Nitrox, for more uniformity

moved "nitrox" to TPTP

generalize type of List.listrel

support for Ex1 in quickcheck-narrowing

adding another internal constant to mutabelle's blacklust

adding some more forbidden constant names for the mutated conjecture generation

adding code generation for some list relations

adding fun_eq_iff to the preprocessing

random instance for sets

more configurations to mutabelle

catching code generation errors in quickcheck-narrowing

adding narrowing instance for sets

shortened definitions by adding some termify constants

tuned

adding check_all instance for sets; tuned

tuned

tuned

minor edits in docs

renamed "sound" option to "strict"

updated Sledge docs some more

more doc updates

updated docs

lower timeout for preplay, now that we have more preplay methods

cleanly separate each Metis encoding

basic setup for equational reasoning; updated rewrite_goals_tac and fold_goals_tac;

tuned;

updated examples for syntax translations;

updated section on raw syntax; misc tuning;

updated section about syntax ambiguity;

updated/unified section on mixfix annotations;

tuned;

more on explicit notation;

more accurate Pure grammar;

more refs;

simplified mixfix (NB: infix is no longer required separately);

updated section on print modes;

misc tuning and reformatting; more antiquotations;

clarified syntax section structure;

discontinued obscure history commands;

misc tuning and reformatting;

discontinued obscure history commands;

updated hint about asm_rl;

updated thin_tac;

updated distinct_subgoals_tac, flexflex_tac;

removed obscure material;

updated rotate_tac;

tuned;

updated citations;

updated subgoal_tac;

tuned sectioning;

updated "Control and search tacticals" (moved from ref to implementation); discontinued odd trace flags that assume sequential TTY loop; discontinued obscure DETERM_UNTIL_SOLVED; discontinued obsolete chapter "Tacticals" (ref);

obsolete -- covered in implementation manual;

moved HEADGOAL; added RANGE;

removed some obscure material; misc tuning;

added SELECT_GOAL;

tuned;

updated "subgoal quantifiers";

tuned ML infixes;

document antiquotations for ML infix operators;

tuned;

updated repetition tacticals; discontinued odd trace_REPEAT (assumes sequential TTY loop);

updated THEN, ORELSE, APPEND, and derivatives; discontinued obscure INTLEAVE;

removed obscure/outdated material;