augment Isabelle home directory more systematically;

Cygwin setup via the quasi-mirror isabelle.in.tum.de, which serves a fixed (downgraded) version;

prevent change of directory, by pretending we are the "Command Here" utility;

typo

the perennial doc problem of how to define lists a second time

smoother handling of conjecture, so that its Skolem constants get displayed in countermodels

updated doc

add a timeout on the monotonicity check

handle TPTP definitions as definitions in Nitpick rather than as axioms

get rid of old parser, hopefully for good

fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")

run Mirabelle in quick and dirty mode

doc update

scrollable text;

bundle Cygwin-Terminal.bat; tuned;

basic Cygwin-Terminal for main Isabelle directory;

moved to ~isatest/.bashrc to accomodate AFP;

merged

merged

doc update

NEWS

typedef with implicit set definition is considered legacy;

more standard method setup;

CONTRIBUTORS

added useful Trueprop_conv

move MRSL to a separate file

avoid conflict of Isabelle vs. Isabelle.exe on Cygwin;

more notes on Cygwin, notably for downgrading to 1.7.9 to avoid multi-threading instabilities starting with 1.7.10 early 2012;

CONTRIBUTORS

reworked Probability theory

updated test;

improved non-interpretation of constants and numbers; improved interpretation of terms and formulas; tuned;

improved interpreting conditionals; tuned;

disabled interpreting arithmetic;

improved handling of single-quoted names;

disabled exception packaging in tptp;

moved function for testing problem-name parsing; list of TPTP test files not immediately evaluated;

removed redundant function;

bundle Isabelle.exe;

tuned precedence order of transfer rules

updated generated files;

updated const "relcomp";

merged

add transfer rule for set difference

support Cygwin cold-start via Isabelle.exe, assuming layout of bundle;

merged

merged

adapt to changes in generated transfer rules (cf. 4483c004499a)

fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)

more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);

merged

fixed typos

tried harder to make SML/NJ happy

added timeout argument to TPTP tools

fix bug where "==" was used instead of "HOL.eq"

more meaningful default value

handle exception (needed to solve TPTP problem SEU880^5)

pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.;

refer to isabelle.Main application wrapper;

display return code like Isabelle.app on Mac OS;

default Isabelle application wrapper -- JVM entry point for Isabelle.exe;

updated Isabelle.exe specification, assuming layout of bundle;

USER_HOME settings variable points to cross-platform user home directory;

new example theory for quotient/transfer

update NEWS for transfer/quotient

enable variant of transfer method that proves an implication instead of an equivalence

moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator

merged

NEWS for transfer, lifting, and quotient

new example theory for transfer package

some builtin session timing;

move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose

tuned proofs

add transfer rule for List.set

remove duplicate of lemma id_transfer

added covariant relator set_rel, with transfer rules for set operations

renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator

tried to make SML/NJ happy

tuned "max_relevant" defaults for SMT solvers based on Judgment Day

prepend PWD to relative paths

reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures

swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations

new transfer package rules and lifting setup for lists

strengthen rule list_all2_induct

more standard Theory_Data setup; keep meta-comments within the history;

merged

add transfer rule for nat_case

uniform naming scheme for transfer rules

rename 'correspondence' method to 'transfer_prover'

hide the invariant constant for relators: invariant_commute infrastracture

improved interleaving of start_execution vs. cancel_execution of the next update;

tuned proofs;

always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;

tuned;

simplified internal actor protocol;

builtin timing for main operations;

add secondary transfer rule for universal quantifiers on non-bi-total relations

move definition of set_rel into Library/Quotient_Set.thy

add transfer rule for 'id'

add new transfer rules and setup for lifting package

setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq

NEWS

hide code generation facts in the Float theory, they are only exported for Approximation

merged

forgot to add file

make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules

merged

NEWS

transfer now handles Let

merged

added revised version of Abs_Int

add transfer rule for Let