isabelle: Graph

tuned signature (again) -- keep Properties more generic;
2013-01-17, by wenzelm
tuned proofs;
2013-01-17, by wenzelm
simplified prove of compact_imp_bounded
2013-01-17, by hoelzl
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
2013-01-17, by hoelzl
move auxiliary lemma to top
2013-01-17, by hoelzl
add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite
2013-01-17, by hoelzl
group compactness-eq-seq-compactness lemmas together
2013-01-17, by hoelzl
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
2013-01-17, by hoelzl
tuned
2013-01-17, by hoelzl
removed subseq_bigger (replaced by seq_suble)
2013-01-17, by hoelzl
countablility of finite subsets and rational numbers
2013-01-17, by hoelzl
generalize compact_path_image to topological_space
2013-01-17, by hoelzl
re-generated components.sha1;
2013-01-17, by wenzelm
merged
2013-01-17, by wenzelm
more system-independent order of components.sha1 to keep changes monotonic;
2013-01-17, by wenzelm
clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
2013-01-17, by wenzelm
delay to give users a chance to see what was happening, even with auto_close enabled;
2013-01-17, by wenzelm
updated docs
2013-01-17, by blanchet
updated component again, as there was an issue with hard-coded paths in "runepar.pl"
2013-01-17, by blanchet
added E-Par support
2013-01-17, by blanchet
updated E component
2013-01-17, by blanchet
tweaked defaults
2013-01-17, by blanchet
changed type of preplay time; tuned preplaying
2013-01-17, by smolkas
move preplaying to own structure
2013-01-17, by smolkas
register SHA1 for Haskabelle-2013 component
2013-01-17, by noschinl
register Haskabelle as a component
2013-01-17, by noschinl
merged
2013-01-16, by wenzelm
tuned proofs;
2013-01-16, by wenzelm
tuned proofs;
2013-01-16, by wenzelm
tuned signature;
2013-01-16, by wenzelm
proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
2013-01-16, by wenzelm
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
2013-01-16, by wenzelm
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16, by wenzelm
eliminated dead code;
2013-01-16, by wenzelm
proper range position;
2013-01-16, by wenzelm
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16, by wenzelm
tuned comments;
2013-01-16, by wenzelm
tuned signature;
2013-01-16, by wenzelm
use Pure instead of HOL connectives
2013-01-16, by smolkas
graceful failure
2013-01-16, by blanchet
honor fact range for MePo as well
2013-01-16, by blanchet
more improvements to Isar proof reconstructions
2013-01-15, by blanchet
tuned whitespace
2013-01-15, by blanchet
merged
2013-01-15, by wenzelm
avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
2013-01-15, by wenzelm
tuned;
2013-01-15, by wenzelm
separate color ranges by 1px to improve discernment of overall theory status;
2013-01-15, by wenzelm
grand-unified Admin/Release/build script (excluding .app and .exe);
2013-01-15, by wenzelm
generalized more topology theorems
2013-01-15, by huffman
generalize lemma islimpt_finite to class t1_space
2013-01-14, by huffman
tuned
2013-01-15, by nipkow
more prominent status ticks;
2013-01-14, by wenzelm
merged
2013-01-14, by wenzelm
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
2013-01-14, by wenzelm
include /isabelle/rebaseall in autorebaseall, which is run after installation of further packages;
2013-01-14, by wenzelm
do not register quasi-components, notably cygwin;
2013-01-14, by wenzelm
updated to jdk-7u11;
2013-01-14, by wenzelm
updated to cygwin-20130114;
2013-01-14, by wenzelm
clarified paths: init relatively to cygwin root;
2013-01-14, by wenzelm
avoid odd copies of local configuration or backup files;
2013-01-14, by wenzelm
more precise relevant_range to exploit overview_limit better;
2013-01-14, by wenzelm
restrict "bad" markup to command keyword, notably excluding subsequent comments;
2013-01-14, by wenzelm
differentiate (cover) compactness and sequential compactness
2013-01-14, by hoelzl
introduce first_countable_topology typeclass
2013-01-14, by hoelzl
move prod instantiation of second_countable_topology to its definition
2013-01-14, by hoelzl
renamed countable_basis_space to second_countable_topology
2013-01-14, by hoelzl
move eventually_Ball_finite to Limits
2013-01-14, by hoelzl
more update on Lifting in isar-ref
2013-01-14, by kuncar
NEWS
2013-01-14, by kuncar
update isar-ref for Quotient and Lifting package
2013-01-14, by kuncar
run Sledgehammer provers in parallel in "try"
2013-01-14, by blanchet
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
2013-01-14, by blanchet
adjust weights -- sorts are prolific, so tone them down even more
2013-01-14, by blanchet
merged
2013-01-13, by wenzelm
merged
2013-01-13, by wenzelm
more exhaustive full test, to avoid surprises with makedist_library;
2013-01-13, by wenzelm
hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
2013-01-13, by wenzelm
don't learn theories -- this option is very slow and not very helpful
2013-01-13, by blanchet
more informative output
2013-01-13, by blanchet
have Mirabelle produce more output
2013-01-13, by blanchet
tuned message
2013-01-13, by blanchet
merged
2013-01-13, by wenzelm
updated makedist_library;
2013-01-13, by wenzelm
some attempts to avoid "._" files on Mac OS X;
2013-01-13, by wenzelm
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
2013-01-13, by wenzelm
honor unknown chained in MaSh and a few other tweaks
2013-01-13, by blanchet
remove obsolete MaSh files
2013-01-13, by blanchet
don't generate queries with empty dependency list
2013-01-13, by blanchet
cleaned up hint handling
2013-01-13, by blanchet
better handlig of built-ins -- at the top-level, not in subterms
2013-01-13, by blanchet
tuned message;
2013-01-12, by wenzelm
proper window title;
2013-01-12, by wenzelm
add icon for toplevel windows;
2013-01-12, by wenzelm
lower bound to font size for the sake of Mac OS X (cf. 4cd2d090be8f);
2013-01-12, by wenzelm
forced scroll to bottom, for improved cross-platform appearance;
2013-01-12, by wenzelm
merged
2013-01-12, by wenzelm
tuned font size, notably for current HD displays;
2013-01-12, by wenzelm
more uniform Pretty.char_width;
2013-01-12, by wenzelm
tuned build_dialog: auto_close checkbox avoids user sitting and waiting;
2013-01-12, by wenzelm
tuned signature;
2013-01-12, by wenzelm
more uniform theory progress in build -v and build_dialog;
2013-01-12, by wenzelm
immediate theory progress for build_dialog;
2013-01-12, by wenzelm
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
2013-01-12, by wenzelm
removed unused/non-portable bash_output_fifo;
2013-01-12, by wenzelm
tuned signature;
2013-01-12, by wenzelm
honor filtering out of arguments for built-in constants (e.g. representation of numerals)
2013-01-12, by blanchet
new version of MaSh Python component
2013-01-12, by blanchet
prefer MS-DOS-style temp;
2013-01-11, by wenzelm
more Cygwin packages to help out in a pitch -- NB: make is still needed for legacy usedir;
2013-01-11, by wenzelm
merged
2013-01-11, by wenzelm
more NEWS;
2013-01-11, by wenzelm
proper path names;
2013-01-11, by wenzelm
refer to cygwin mirror with static copy of setup.ini;
2013-01-11, by wenzelm
discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
2013-01-11, by wenzelm
obsolete;
2013-01-11, by wenzelm
more standard contrib/cygwin location (again);
2013-01-11, by wenzelm
updated messages
2013-01-11, by blanchet
fixed escaping for MeSh encoder
2013-01-11, by blanchet
don't learn from the proof of "psimps" etc.
2013-01-11, by blanchet
updated MaSh Python component
2013-01-11, by blanchet