isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things
2012-04-25, by blanchet
output SZS status as early as possible
2012-04-25, by blanchet
sorted lemma list in NEWS
2012-04-25, by hoelzl
merged
2012-04-25, by wenzelm
reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2);
2012-04-25, by wenzelm
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
2012-04-25, by wenzelm
updated README;
2012-04-25, by wenzelm
include generated application wrapper;
2012-04-25, by wenzelm
back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer;
2012-04-25, by wenzelm
ISABELLE_JDK_HOME is already provided by isatest shell environment;
2012-04-25, by wenzelm
added splash screen, to reduce confusion when waiting for main application to start up;
2012-04-25, by wenzelm
move polyml within Cygwin /usr/local to simplify its rebasing;
2012-04-25, by wenzelm
improved spelling;
2012-04-25, by wenzelm
added "no_atp"s for extremely prolific, useless facts for ATPs
2012-04-25, by blanchet
tuned;
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
made "split_last" more robust in the face of obscure low-level errors
2012-04-24, by blanchet
removed confusing error
2012-04-24, by blanchet
some friendly message;
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
merged
2012-04-24, by wenzelm
merged
2012-04-24, by sultana
merged
2012-04-24, by sultana
reversed Tools to Actions Mirabelle renaming;
2012-04-24, by sultana
tuned;
2012-04-24, by sultana
reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
2012-04-24, by blanchet
doc update
2012-04-24, by nipkow
prefer evince over old xpdf -- NB: x86-cygwin bundles its own application;
2012-04-24, by wenzelm
cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
2012-04-24, by wenzelm
chmod -x;
2012-04-24, by wenzelm
augment Isabelle home directory more systematically;
2012-04-24, by wenzelm
Cygwin setup via the quasi-mirror isabelle.in.tum.de, which serves a fixed (downgraded) version;
2012-04-24, by wenzelm
prevent change of directory, by pretending we are the "Command Here" utility;
2012-04-24, by wenzelm
typo
2012-04-24, by nipkow
the perennial doc problem of how to define lists a second time
2012-04-24, by nipkow
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
2012-04-24, by blanchet
updated doc
2012-04-24, by blanchet
add a timeout on the monotonicity check
2012-04-24, by blanchet
handle TPTP definitions as definitions in Nitpick rather than as axioms
2012-04-24, by blanchet
get rid of old parser, hopefully for good
2012-04-24, by blanchet
fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)")
2012-04-24, by blanchet
run Mirabelle in quick and dirty mode
2012-04-24, by blanchet
doc update
2012-04-24, by nipkow
scrollable text;
2012-04-23, by wenzelm
bundle Cygwin-Terminal.bat;
2012-04-23, by wenzelm
basic Cygwin-Terminal for main Isabelle directory;
2012-04-23, by wenzelm
moved to ~isatest/.bashrc to accomodate AFP;
2012-04-23, by wenzelm
merged
2012-04-23, by wenzelm
merged
2012-04-23, by nipkow
doc update
2012-04-23, by nipkow
NEWS
2012-04-23, by krauss
typedef with implicit set definition is considered legacy;
2012-04-23, by wenzelm
more standard method setup;
2012-04-23, by wenzelm
CONTRIBUTORS
2012-04-23, by kuncar
added useful Trueprop_conv
2012-04-23, by kuncar
move MRSL to a separate file
2012-04-23, by kuncar
avoid conflict of Isabelle vs. Isabelle.exe on Cygwin;
2012-04-23, by wenzelm
more notes on Cygwin, notably for downgrading to 1.7.9 to avoid multi-threading instabilities starting with 1.7.10 early 2012;
2012-04-23, by wenzelm
CONTRIBUTORS
2012-04-23, by hoelzl
reworked Probability theory
2012-04-23, by hoelzl
updated test;
2012-04-23, by sultana
improved non-interpretation of constants and numbers;
2012-04-23, by sultana
improved interpreting conditionals;
2012-04-23, by sultana
disabled interpreting arithmetic;
2012-04-23, by sultana
improved handling of single-quoted names;
2012-04-23, by sultana
disabled exception packaging in tptp;
2012-04-23, by sultana
moved function for testing problem-name parsing;
2012-04-23, by sultana
removed redundant function;
2012-04-23, by sultana
bundle Isabelle.exe;
2012-04-22, by wenzelm
tuned precedence order of transfer rules
2012-04-22, by huffman
updated generated files;
2012-04-22, by wenzelm
updated const "relcomp";
2012-04-22, by wenzelm
merged
2012-04-22, by wenzelm
add transfer rule for set difference
2012-04-22, by huffman
support Cygwin cold-start via Isabelle.exe, assuming layout of bundle;
2012-04-22, by wenzelm
merged
2012-04-22, by wenzelm
merged
2012-04-22, by huffman
adapt to changes in generated transfer rules (cf. 4483c004499a)
2012-04-22, by huffman
fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)
2012-04-22, by huffman
more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
2012-04-22, by wenzelm
merged
2012-04-22, by wenzelm
fixed typos
2012-04-22, by blanchet
tried harder to make SML/NJ happy
2012-04-22, by blanchet
added timeout argument to TPTP tools
2012-04-22, by blanchet
fix bug where "==" was used instead of "HOL.eq"
2012-04-22, by blanchet
more meaningful default value
2012-04-22, by blanchet
handle exception (needed to solve TPTP problem SEU880^5)
2012-04-22, by blanchet
pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.;
2012-04-22, by wenzelm
refer to isabelle.Main application wrapper;
2012-04-22, by wenzelm
display return code like Isabelle.app on Mac OS;
2012-04-22, by wenzelm
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
2012-04-22, by wenzelm
updated Isabelle.exe specification, assuming layout of bundle;
2012-04-22, by wenzelm
USER_HOME settings variable points to cross-platform user home directory;
2012-04-22, by wenzelm
new example theory for quotient/transfer
2012-04-22, by huffman
update NEWS for transfer/quotient
2012-04-21, by huffman
enable variant of transfer method that proves an implication instead of an equivalence
2012-04-21, by huffman
moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
2012-04-19, by haftmann
merged
2012-04-21, by wenzelm
NEWS for transfer, lifting, and quotient
2012-04-21, by huffman
new example theory for transfer package
2012-04-21, by huffman
some builtin session timing;
2012-04-21, by wenzelm
move alternative definition lemmas into Lifting.thy;
2012-04-21, by huffman
tuned proofs
2012-04-21, by huffman
add transfer rule for List.set
2012-04-21, by huffman
remove duplicate of lemma id_transfer
2012-04-21, by huffman
added covariant relator set_rel, with transfer rules for set operations
2012-04-21, by huffman
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
2012-04-21, by huffman
tried to make SML/NJ happy
2012-04-21, by blanchet
tuned "max_relevant" defaults for SMT solvers based on Judgment Day
2012-04-21, by blanchet
prepend PWD to relative paths
2012-04-21, by blanchet
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
2012-04-21, by blanchet
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
2012-04-21, by blanchet
new transfer package rules and lifting setup for lists
2012-04-21, by huffman
strengthen rule list_all2_induct
2012-04-21, by huffman
more standard Theory_Data setup;
2012-04-20, by wenzelm
merged
2012-04-20, by wenzelm
add transfer rule for nat_case
2012-04-20, by huffman
uniform naming scheme for transfer rules
2012-04-20, by huffman
rename 'correspondence' method to 'transfer_prover'
2012-04-20, by huffman
hide the invariant constant for relators: invariant_commute infrastracture
2012-04-20, by kuncar