tuned;

merged

make more simp rules respect int/bin distinction

make bool list functions respect int/bin distinction

merged;

tuned;

clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;

further graph operations from ML;

removed dead code;

directed graphs (in Scala);

make uses of bin_split respect int/bin distinction

remove lemma bin_cat_Pls, which doesn't respect int/bin distinction

make uses of constant bin_sc respect int/bin distinction

remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc

remove unused lemmas

simplify proofs

make uses of bin_sign respect int/bin distinction

removed unnecessary lemma zero_bintrunc

remove unnecessary lemmas

removed unnecessary constant bin_rl

remove duplication of lemmas bin_{rest,last}_BIT

remove lemmas Bit{0,1}_div2

simplify proof

deal with FIXMEs for linarith examples

CONTRIBUTORS

merged

tuned whitespace

tuned whitespace

adding documentation about find_unused_assms command and use_subtype option in the IsarRef

NEWS

adding some examples with find_unused_assms command

adding new command "find_unused_assms"

removing some unnecessary premises from Map theory

preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)

generalizing inj_on_Int

moving Quickcheck's example to its own session

tuned proofs;

more robust visible_range: allow empty view;

misc tuning;

merged;

made SML/NJ happy;

tuned proofs;

merged

tuned proofs;

approximate Perspective.full within the bounds of the JVM;

misc tuning; more indentation;

invoke later to reduce chance of causing deadlock;

misc tuning; more indentation;

separate module for text status overview;

overview.delay_repaint: avoid wasting GUI cycles via update_delay; prefer delay_first for prover initiated events -- avoid indefinite delay;

tuned;

merged

merged

Fixed bugs: - set_env no longer modifies pfuns field in theory data record. Instead, a copy of this field is now contained in the env field. - add_type_def now checks whether type associated with SPARK enumeration type is really a datatype with no parameters. - check_pfuns_types now properly strips off prefixes of proof function names.

merged

subtype preprocessing in Quickcheck; adding option use_subtype; tuned

adding parsing of an optional predicate with quickcheck_generator command

updated generated files (cf. 8d51b375e926);

merged;

add missing lemmas to compute_div_mod

remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)

avoid using constant Int.neg

renamed ex/Numeral.thy to ex/Numeral_Representation.thy

reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems

tuned whitespace

tuned proof

tuned proof

distributed lattice properties of predicates to places of instantiation

removing some unnecessary premises from Divides

simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)

observe HEIGHT of overview ticks; misc tuning and clarification;

more careful painting of overview component: more precise and more efficient;

clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;

use qualified constant names instead of suffixes (from Florian Haftmann)

tuned proofs

tuned

brute-force adjustion

tuned whitespace

tuned

tuned

tuned code

dropped whitespace

dropped dead code

dropped dead code

dropped dead code

dropped dead code

dropped dead code

dropped dead code

corrected typo

dropped dead code

notepad is more appropriate here

corrected treatment of applications of built-in functions to higher-order terms

NEWS

merged

added congruence rules for Option.{map|bind}

updated generated documents

avoid redefinition of @{theory} antiquotation

update of generated documents

tuned whitespace

clarified

corrected spelling

clarified

more precise semantics of "theory" antiquotation

tuned import

dropped references to obsolete theories

adjusted to set type constructor

tuned whitespace

more explicit error on malformed abstract equation; dropped dead code; tuned signature

simplified configuration options for syntax ambiguity;

retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);

more antiquotations;

more symbols; misc tuning;

tuned imports;

tuned proofs;

simplified configuration options for syntax ambiguity;

merged

removing unnecessary premise from diff_single_insert

explicit is better than implicit;

more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X);

simplifying proof

removing unnecessary premises in theorems of List theory

tuning mutabelle script

adding documentation for abort_potential option in quickcheck

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);

uniform Isar source formatting for this file;

clarified outer syntax "constdecl", which is only local to some rail diagrams;

discontinued obsolete "prems" fact;

eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);

removed obsolete files;

more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba);

removed dead code;

updated listrel (cf. 80dccedd6c14);

removed redundant cut_inst_tac -- already covered in implementation manual;

updated rewrite_goals_rule, rewrite_rule;

NEWS;

updated refs;

renamed "xstr" to "str_token";

merged

don't report spurious LEO-II errors

better error message

removing debug code in mutabelle

adding abort_potential functionality in quickcheck

adding abort_potential configuration in Quickcheck

clarified bires_inst_tac: retain internal exceptions;

tuned signature;

more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;

more conventional tactic setup;

eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);

prefer high-level elim_format;

discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;

method setup;

simplified use of tacticals;

comment;

tuned signature, according to actual usage of these operations;

tuned signature;

normalized aliases;

elininated unused INTLEAVE;

eliminated unused rewrite_goal_rule;

eliminated unused subgoals_tac;

eliminated obsolete aliases;

eliminated obsolete aliases;

tuned;

merged, resolving trivial conflicts;

merged;

new SPASS options

making num_mutations a configuration that can be changed with the mutabelle bash command

making max_mutants an option that can be changed in the Mutabelle-script

increase timeout to 30 seconds; changing mutabelle script

parse clauses generated from several formulas

be more gentle when generating KBO weights

update SPASS slices

more specification of the quotient package in IsarRef

specification of the quotient package

tune KBO weight code

minor DFG fix

new SPASS slices

improved KBO weights -- beware of explicit applications

added possibility of generating KBO weights to DFG problems

Generalize the compositional preservation theorems

use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")

removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly

beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms

fixed arity error

tuning

renamed type encoding

adding some forbidden constant names for mutabelle

mutabelle ignores theorems with internal constants

tuned

merged

simplified code generation

remove option that's on by default

no need for a script/mega-hack with the new SPASS

cleaned up new SPASS parsing

tuning

merged

adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists

tuning to remove ML warnings

removed double filtering of type args

adding a quickcheck example about functions and sets

removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)

adding a remark about lemma which is too special and should be removed

another try to improve code generation of set equality (cf. da32cf32c0c7)

beautifying definitions of check_all and adding instance for finite_4

Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.

added option to Mirabelle/Sledgehammer

improved hashing w.r.t. Mirabelle, to help debugging

tuned SPASS DFG output

the new SPASS gives accurate fact information, so no need for old hack anymore

fixed docs

made sure to filter type args also for "uncurried alias" equations

made option available to users (mostly for experiments)

using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)

optimization: slice caching in case two consecutive slices are nearly identical

extended SPASS/DFG output with ranks

try to pass fewer options to Metis

Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat

improve SPASS scripts

change 9ce354a77908 wasn't quite right -- here's an improvement

better SPASS setup

don't introduce new symbols in helpers -- makes problems unprovable

only constants can be aliased

include new SPASS by default if available

adding an example for finite and cofinite sets

adding a minimally refined equality on sets for code generation

adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type

improving code equations for multisets that violated the distinct AList abstraction

tuning

implemented partial application aliases (for SPASS mainly)

really fixed syntax bug in DFG output (cf. ef62c2fafa9e)

don't stumble on SPASS debug output

tuning

proper statuses for "fact_from_ref"

tuned

renamed Sledgehammer option

third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)

improve SPASS setup

adding code equation for setsum

avoid name clash, really

fixed syntax bug in DFG output

new SPASS setup

distinguish between ":lr" and ":lt" (terminating) in DFG format

nicer keyword class avoidance scheme

new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)

mutabelle must handle the case where quickcheck returns multiple results

reverted e2b1a86d59fc -- broke Metis's lambda-lifting

merged

NEWS

added "'a rel"

fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers

new SPASS setup

example tuning

implemented new lambda translations scheme

avoid unsupported case in Metis

docs and news

rename lambda translation schemes

example tuning

NEWS

renaming all lemmas with name rel_pow to relpow

adding code equations for max_extp and mlex

adding code generation for relpow by copying the ideas for code generation of funpow

adding code equation for rtranclp in Enum

adding code equation for max_ext

adding code equation for tranclp

adding code_unfold to make measure executable

removed accidental dependance of abstract interpreter on gamma

merged

tuned

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;

updated RSN, RL, RLN, MRS; discontinued obscure MRL;

removed obscure/outdated material;

tuned;

more on Logic.all/mk_implies etc.;

reduce AFP test by many hours;

added termination of narrowing

really need 64bit here; prefer explicit version information for contrib;

Added termination proof for widening

switch afp test to Darwin on macbroy2

merged

introduced commands over a set of vars

basic support for PIDE Scala programming, independently of the main Isabelle repository;

fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick

updated message

improve installation instructions

allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script

factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero

refreshing NEWS

renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)

renamed theory AList to DAList