isabelle: Graph

old-style numbered structure index is legacy feature (hardly ever used now);
2011-08-22, by wenzelm
added official Text.Range.Ordering;
2011-08-22, by wenzelm
tuned signature;
2011-08-22, by wenzelm
reverted some odd changes to HOL/Import (cf. 74c08021ab2e);
2011-08-22, by wenzelm
merged
2011-08-22, by krauss
modernized specifications
2011-08-21, by krauss
removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
2011-08-21, by krauss
removed technical or trivial unused facts
2011-08-21, by krauss
more precise authors and comments;
2011-08-21, by krauss
added proof of idempotence, roughly after HOL/Subst/Unify.thy
2011-08-21, by krauss
tuned proofs, sledgehammering overly verbose parts
2011-08-21, by krauss
tuned notation
2011-08-21, by krauss
ported some lemmas from HOL/Subst/*;
2011-08-21, by krauss
changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
2011-08-21, by krauss
merged
2011-08-21, by huffman
add lemmas interior_Times and closure_Times
2011-08-21, by huffman
avoid pred/set mixture
2011-08-21, by haftmann
avoid pred/set mixture
2011-08-21, by haftmann
merged
2011-08-21, by wenzelm
remove unnecessary euclidean_space class constraints
2011-08-21, by huffman
section -> subsection
2011-08-21, by huffman
scale dependency graph to fit on page
2011-08-21, by huffman
more robust initialization of token marker and line context wrt. session startup;
2011-08-21, by wenzelm
tuned Parse.group: delayed failure message;
2011-08-21, by wenzelm
avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
2011-08-21, by wenzelm
default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
2011-08-21, by wenzelm
tuned;
2011-08-21, by wenzelm
discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
2011-08-21, by wenzelm
discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
2011-08-21, by wenzelm
merged
2011-08-21, by wenzelm
replace lemma realpow_two_diff with new lemma square_diff_square_factored
2011-08-20, by huffman
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-20, by huffman
move lemma add_eq_0_iff to Groups.thy
2011-08-20, by huffman
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
2011-08-20, by huffman
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
2011-08-20, by huffman
add lemma power2_eq_iff
2011-08-20, by huffman
remove some over-specific rules from the simpset
2011-08-20, by huffman
merged
2011-08-20, by huffman
redefine constant 'trivial_limit' as an abbreviation
2011-08-20, by huffman
purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
2011-08-21, by wenzelm
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
2011-08-21, by wenzelm
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
2011-08-20, by wenzelm
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-20, by wenzelm
clarified get_imports -- should not rely on accidental order within graph;
2011-08-20, by wenzelm
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
2011-08-20, by wenzelm
discontinued "Interrupt", which could disturb administrative tasks of the document model;
2011-08-20, by wenzelm
more direct balanced version Ord_List.unions;
2011-08-20, by wenzelm
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
2011-08-20, by wenzelm
tuned future priorities (again);
2011-08-20, by wenzelm
clarified fulfill_norm_proof: no join_thms yet;
2011-08-20, by wenzelm
added Future.joins convenience;
2011-08-20, by wenzelm
merged
2011-08-20, by haftmann
deactivated »unknown« nitpick example
2011-08-20, by haftmann
merged
2011-08-20, by haftmann
tuned proof
2011-08-20, by haftmann
more uniform formatting of specifications
2011-08-20, by haftmann
compatibility layer
2011-08-20, by haftmann
merged
2011-08-20, by haftmann
more concise definition for Inf, Sup on bool
2011-08-19, by haftmann
do not call ghc with -fglasgow-exts
2011-08-18, by noschinl
remove some redundant simp rules about sqrt
2011-08-19, by huffman
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
2011-08-19, by huffman
remove unused lemma DERIV_sin_add
2011-08-19, by huffman
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-08-19, by huffman
remove redundant lemma exp_ln_eq in favor of ln_unique
2011-08-19, by huffman
merged
2011-08-19, by huffman
Lim.thy: legacy theorems
2011-08-19, by huffman
SEQ.thy: legacy theorem names
2011-08-19, by huffman
delete unused lemmas about limits
2011-08-19, by huffman
Transcendental.thy: add tendsto_intros lemmas;
2011-08-19, by huffman
add lemma isCont_tendsto_compose
2011-08-19, by huffman
merged
2011-08-19, by wenzelm
Transcendental.thy: remove several unused lemmas and simplify some proofs
2011-08-19, by huffman
remove unused lemmas
2011-08-19, by huffman
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
2011-08-19, by huffman
remove some redundant simp rules
2011-08-19, by huffman
maintain recent future proofs at transaction boundaries;
2011-08-19, by wenzelm
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
2011-08-19, by wenzelm
tuned;
2011-08-19, by wenzelm
tuned signature (again);
2011-08-19, by wenzelm
tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19, by wenzelm
refined Future.cancel: explicit future allows to join actual cancellation;
2011-08-19, by wenzelm
Future.promise: explicit abort operation (like uninterruptible future job);
2011-08-19, by wenzelm
editable raw text areas: allow user to clear content;
2011-08-19, by wenzelm
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
2011-08-19, by wenzelm
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-19, by wenzelm
clarified Future.cond_forks: more uniform handling of exceptional situations;
2011-08-19, by wenzelm
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
2011-08-19, by Cezary Kaliszyk
merged
2011-08-18, by huffman
define complex exponential 'expi' as abbreviation for 'exp'
2011-08-18, by huffman
remove more bounded_linear locale interpretations (cf. f0de18b62d63)
2011-08-18, by huffman
optimize some proofs
2011-08-18, by huffman
add Multivariate_Analysis dependencies
2011-08-18, by huffman
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
2011-08-18, by huffman
declare euclidean_component_zero[simp] at the point it is proved
2011-08-18, by huffman
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
2011-08-19, by Cezary Kaliszyk
merged;
2011-08-18, by wenzelm
merged
2011-08-18, by huffman
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-18, by huffman
merged
2011-08-18, by haftmann
merged
2011-08-18, by haftmann
avoid duplicated simp add option
2011-08-18, by haftmann
observe distinction between sets and predicates more properly
2011-08-18, by haftmann
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-08-18, by haftmann
avoid case-sensitive name for example theory
2011-08-18, by haftmann
merged
2011-08-18, by nipkow
case_names NEWS
2011-08-18, by nipkow
adding documentation about simps equation in the inductive package
2011-08-18, by bulwahn
activating narrowing-based quickcheck by default
2011-08-18, by bulwahn
more precise treatment of exception nesting and serial numbers;
2011-08-18, by wenzelm
more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18, by wenzelm
updated sequential version (cf. b94951f06e48);
2011-08-18, by wenzelm
tuned comments;
2011-08-18, by wenzelm
tuned document;
2011-08-18, by wenzelm
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
2011-08-18, by wenzelm
export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
2011-08-18, by wenzelm
tune Par_Exn.make: balance merge;
2011-08-18, by wenzelm
Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
2011-08-18, by Cezary Kaliszyk
merged
2011-08-17, by huffman
HOL-IMP: respect set/pred distinction
2011-08-17, by huffman
Determinants.thy: avoid using mem_def/Collect_def
2011-08-17, by huffman
Wfrec.thy: respect set/pred distinction
2011-08-17, by huffman
follow updates of Isabelle/Pure;
2011-08-18, by wenzelm
merged
2011-08-17, by wenzelm
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
2011-08-17, by huffman
merged
2011-08-17, by huffman
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
2011-08-17, by huffman
add lemma tendsto_compose_eventually; use it to shorten some proofs
2011-08-17, by huffman
Topology_Euclidean_Space.thy: simplify some proofs
2011-08-17, by huffman
add lemma metric_tendsto_imp_tendsto
2011-08-17, by huffman
simplify proofs of lemmas open_interval, closed_interval
2011-08-17, by huffman
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-08-17, by wenzelm
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
2011-08-17, by wenzelm
more systematic handling of parallel exceptions;
2011-08-17, by wenzelm
tuned signature;
2011-08-17, by wenzelm
merged
2011-08-17, by haftmann
merged
2011-08-17, by haftmann
merged
2011-08-17, by haftmann
avoid Collect_def in proof
2011-08-16, by haftmann
modernized signature of Term.absfree/absdummy;
2011-08-17, by wenzelm
improved default context for ML toplevel pretty-printing;
2011-08-17, by wenzelm
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
2011-08-17, by wenzelm
some convenience actions/shortcuts for control symbols;
2011-08-17, by wenzelm
export Function_Fun.fun_config for user convenience;
2011-08-17, by wenzelm
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
2011-08-17, by wenzelm
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
2011-08-17, by blanchet
merged
2011-08-16, by huffman
add simp rules for isCont
2011-08-16, by huffman
updated keywords -- old codegen is no longer in Pure;
2011-08-16, by wenzelm
include HOL-Library keywords for the sake of recdef;
2011-08-16, by wenzelm
merged
2011-08-16, by wenzelm
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
2011-08-16, by huffman
get Multivariate_Analysis/Determinants.thy compiled and working again
2011-08-16, by huffman
get Library/Permutations.thy compiled and working again
2011-08-16, by huffman
workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16, by wenzelm
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
2011-08-16, by wenzelm
tuned message;
2011-08-16, by wenzelm
more robust treatment of node dependencies in incremental edits;
2011-08-16, by wenzelm
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
2011-08-16, by wenzelm
omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;
2011-08-16, by wenzelm
merged
2011-08-15, by huffman
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
2011-08-15, by huffman
add lemma tendsto_compose
2011-08-15, by huffman
remove extraneous subsection heading
2011-08-15, by huffman
generalized lemma closed_Collect_eq
2011-08-15, by huffman
remove duplicate lemma disjoint_iff
2011-08-15, by huffman
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
2011-08-15, by huffman
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
2011-08-15, by huffman
generalize lemma continuous_uniform_limit to class metric_space
2011-08-15, by huffman
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-15, by huffman
Topology_Euclidean_Space.thy: organize section headings
2011-08-15, by huffman
simplify some proofs
2011-08-15, by huffman
generalize lemma convergent_subseq_convergent
2011-08-14, by huffman
locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
2011-08-14, by huffman
locale-ize some constant definitions, so complete_space can inherit from metric_space
2011-08-14, by huffman
generalize constant 'lim' and limit uniqueness theorems to class t2_space
2011-08-14, by huffman
Quotient Package: make quotient_type work with separate set type
2011-08-16, by Cezary Kaliszyk
updated README;
2011-08-15, by wenzelm
touch descendants of edited nodes;
2011-08-15, by wenzelm
parellel scheduling of node edits and execution;
2011-08-15, by wenzelm
tuned error message;
2011-08-15, by wenzelm
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
2011-08-15, by wenzelm
explicit check of finished evaluation;
2011-08-15, by wenzelm
refined Document.edit: less stateful update via Graph.schedule;
2011-08-15, by wenzelm
simplified exec: eliminated unused status flag;
2011-08-15, by wenzelm
consistently use variable name 'F' for filters
2011-08-14, by huffman
generalize lemmas about LIM and LIMSEQ to tendsto
2011-08-14, by huffman
HOL-Nominal-Examples: respect distinction between sets and functions
2011-08-13, by huffman
less verbosity in batch mode -- spam reduction and notable performance improvement;
2011-08-13, by wenzelm
merged
2011-08-13, by wenzelm
HOL-Hahn_Banach: use Set_Algebras library
2011-08-13, by huffman
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
2011-08-13, by huffman
clarified Toplevel.end_theory;
2011-08-13, by wenzelm
simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13, by wenzelm
simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13, by wenzelm
provide node header via Scala layer;
2011-08-13, by wenzelm
reduced verbosity;
2011-08-13, by wenzelm
tuned signature;
2011-08-13, by wenzelm
clarified node header -- exclude master_dir;
2011-08-13, by wenzelm
tuned;
2011-08-13, by wenzelm
maintain node header;
2011-08-13, by wenzelm
removed unused lemma; removed old-style ;
2011-08-13, by kleing
point isatest-statistics to the right afp log files
2011-08-13, by kleing
IMP/Util distinguishes between sets and functions again; imported only where used.
2011-08-13, by kleing
remove redundant lemma setsum_norm in favor of norm_setsum;
2011-08-12, by huffman
merged
2011-08-12, by huffman
make more HOL theories work with separate set type
2011-08-12, by huffman
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
2011-08-13, by wenzelm
merged
2011-08-12, by wenzelm
merged
2011-08-12, by huffman
make Multivariate_Analysis work with separate set type
2011-08-12, by huffman
make HOLCF work with separate set type
2011-08-12, by huffman
merged
2011-08-12, by huffman
avoid duplicate rule warnings
2011-08-11, by huffman
modify euclidean_space class to include basis set
2011-08-11, by huffman
remove lemma stupid_ext
2011-08-11, by huffman
documented extended version of case_names attribute
2011-08-12, by nipkow
normalized theory dependencies wrt. file_store;
2011-08-12, by wenzelm
general Graph.schedule;
2011-08-12, by wenzelm
allow "$" within basic path elements (NB: initial "$" refers to path variable);
2011-08-12, by wenzelm
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-12, by wenzelm
simplified class Thy_Header;
2011-08-12, by wenzelm
clarified Exn.message;
2011-08-12, by wenzelm
uniform treatment of header edits as document edits;
2011-08-11, by wenzelm