isabelle: Graph

merged
2013-01-17, by wenzelm
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
start using MaSh hints
2013-01-11, by blanchet
always compare theorem using the same, weaker function
2013-01-11, by blanchet
tuned
2013-01-11, by smolkas
set show_markup to false in order to avoid problems in jedit
2013-01-11, by smolkas
merged
2013-01-11, by nipkow
tuned
2013-01-11, by nipkow
merged
2013-01-11, by noschinl
added some ereal_of_enat_* lemmas (from $AFP/thys/Girth_Chromatic)
2013-01-10, by noschinl
explicit references avoid dynamic lookup
2013-01-11, by haftmann
sharing of recursive results on evaluation
2013-01-11, by haftmann
removed debugging code
2013-01-10, by blanchet
make name table work the way it was intended to
2013-01-10, by blanchet
export MeSh data as well
2013-01-10, by blanchet
merged
2013-01-10, by wenzelm
manage cygwin as bundled quasi-component;
2013-01-10, by wenzelm
tuned;
2013-01-10, by wenzelm
outermost directory structure for Windows/Cygwin;
2013-01-10, by wenzelm
updated for release;
2013-01-10, by wenzelm
more general prover termination dialog, which might indicate undetected failure or just ML "exit 0";
2013-01-10, by wenzelm
clarified cygwin/isabelle scripts;
2013-01-10, by wenzelm
more systematic makedist_cygwin;
2013-01-10, by wenzelm
prefer system build mode in main application wrappers, to produce heaps insided distribution directory;
2013-01-10, by wenzelm
tuned proofs;
2013-01-10, by wenzelm
dock "Theories" right, although it might obscure some control buttons;
2013-01-10, by wenzelm
scala-2.9.2 is still supported;
2013-01-10, by wenzelm
made SML/NJ happy;
2013-01-10, by wenzelm
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
2013-01-10, by wenzelm
minor update;
2013-01-09, by wenzelm
purge other platforms uniformly;
2013-01-09, by wenzelm
unconditional jedit_build;
2013-01-09, by wenzelm
Console is not docked on startup;
2013-01-09, by wenzelm
refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist;
2013-01-09, by wenzelm
renamed tool;
2013-01-09, by wenzelm
create required PREFS_DIR;
2013-01-09, by wenzelm
eliminated choosefrom -- power-users may edit global defaults within script;
2013-01-09, by wenzelm
tuned;
2013-01-09, by wenzelm
updated makebundles as Admin isabelle tool;
2013-01-09, by wenzelm
tuned;
2013-01-09, by wenzelm
Added proof function declarations for min and max
2013-01-10, by berghofe
disable interactive mode of Specification.theorem with its slow printing of results;
2013-01-08, by wenzelm
changed exception to uppercase
2013-01-09, by smolkas
proper exception handling; reraise interrupt exceptions
2013-01-09, by smolkas
more CHECKLIST;
2013-01-09, by wenzelm
merged
2013-01-09, by wenzelm
build browser more robustly before startup;
2013-01-09, by wenzelm
standardized treatment of timing properties;
2013-01-09, by wenzelm
consider merging obtain steps
2013-01-09, by smolkas
preplay obtain steps
2013-01-09, by smolkas
tune spelling;
2013-01-09, by wenzelm
include timing properties in log; build_history_base
2013-01-08, by wenzelm
merged
2013-01-08, by wenzelm
upper bound for font size;
2013-01-08, by wenzelm
more tolerant set/pred rule declaration to improve "tool compliance", notably for "context assumes";
2013-01-08, by wenzelm
more aggressive update -- potentially relevant for previously is_outdated output;
2013-01-08, by wenzelm
allow negative argument in "consumes" source format;
2013-01-08, by wenzelm
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
2013-01-08, by wenzelm
more direct invalidateScreenLineRange after changed assignment;
2013-01-08, by wenzelm
tuned;
2013-01-08, by wenzelm
tuned -- prefer high-level Table.merge with its slightly more conservative update;
2013-01-08, by wenzelm
tuned output
2013-01-08, by blanchet
tuned names
2013-01-08, by nipkow
merged;
2013-01-07, by wenzelm
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
2013-01-07, by wenzelm
no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;
2013-01-07, by wenzelm
merged
2013-01-07, by wenzelm
export some generally useful operations;
2013-01-06, by wenzelm
tuned comment -- do not claim anything;
2013-01-07, by wenzelm
cleaner context threading
2013-01-07, by blanchet
tuned output
2013-01-07, by blanchet
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
2013-01-07, by wenzelm
put single-theorem names before multi-theorem ones (broken since 5d147d492792)
2013-01-06, by blanchet
get rid of spurious "Isar" proofs
2013-01-06, by blanchet
also generate queries for goals with too many Isar dependencies
2013-01-06, by blanchet
updated to scala-2.10.0;
2013-01-06, by wenzelm
merged
2013-01-06, by blanchet
tuned message
2013-01-05, by blanchet
tap after, not before command invocation
2013-01-05, by blanchet
increased hard timeout -- minimization can take time
2013-01-05, by blanchet
nicer output
2013-01-05, by blanchet
pass option to minimize
2013-01-05, by blanchet
prefer apple.laf.useScreenMenuBar=true (despite cf. effcfa38e77b) to make it work better with full-screen mode;
2013-01-05, by wenzelm
ignore vacuous edits (e.g. stemming from Plugin.init_models) to avoid pointless protocol round-trip, which could lead to painting of outdated snapshot in the meantime (notably on Windows);
2013-01-05, by wenzelm
tuned JEDIT_JAVA_OPTIONS: increase chances that it works with approx. 8 cores and 32bit platform (notably Windows);
2013-01-05, by wenzelm
propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
2013-01-05, by wenzelm
premature window close means failure;
2013-01-05, by wenzelm
less aggressive Assumption.export_term (similar to Generic_Target.abbrev): merely expand local defs and thus allow notation for local fixes;
2013-01-05, by wenzelm
proper return code on window close;
2013-01-05, by wenzelm
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
2013-01-05, by wenzelm
more direct property names;
2013-01-05, by wenzelm
tuned -- less indirection;
2013-01-05, by wenzelm
tuned blacklisting in relevance filter
2013-01-05, by blanchet
refined class handling, to prevent cycles in fact graph
2013-01-04, by blanchet
learn from low-level, inside-class facts
2013-01-04, by blanchet
tuning
2013-01-04, by blanchet
tweaked nicknames
2013-01-04, by blanchet
merged
2013-01-04, by wenzelm
more reactive completion popup by default;
2013-01-04, by wenzelm
actually install required copy of Highlight.jar;
2013-01-04, by wenzelm
updated to jedit_build-20130104;
2013-01-04, by wenzelm
another attempt to get Mac OS X keyhandling right: ALTERNATIVE_DISPATCHER is off, but ALT_KEY_PRESSED_DISABLED is more careful to interpret ALT like ALT_GRAPH, which does not count as modifier here (NB: CONTROL + ALT means ALT_GRAPH on Windows, but ALT means ALT_GRAPH on Mac OS X);
2013-01-04, by wenzelm
more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
2013-01-04, by wenzelm
tuned imports;
2013-01-04, by wenzelm
support TAB in completion: need to configure the component with the key handler;
2013-01-04, by wenzelm
note to eliminate dynamic name reference
2013-01-04, by haftmann
speed up generation of local theorem nicknames
2013-01-04, by blanchet
speed up nickname generation for local facts
2013-01-04, by blanchet
updated docs
2013-01-04, by blanchet
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
2013-01-04, by blanchet
tweaked fudge factor
2013-01-04, by blanchet
more NEWS;
2013-01-04, by wenzelm
document 'locale_deps';
2013-01-04, by wenzelm
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
2013-01-04, by wenzelm
more formal inlining of system information;
2013-01-04, by wenzelm
tuned message -- suppress inlined system information;
2013-01-04, by wenzelm
merged
2013-01-04, by smolkas
tuned
2013-01-03, by smolkas
avoid long enumeration of HO unifiers;
2013-01-03, by wenzelm
disable search dialog pool on all platforms -- to prevent GUI synchronization problems seen on KDE (e.g. Kubuntu 12.10);
2013-01-03, by wenzelm
merged
2013-01-03, by wenzelm