isabelle: Graph

tuned proofs;
2011-08-24, by wenzelm
tuned syntax -- avoid ambiguities;
2011-08-24, by wenzelm
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
2011-08-24, by wenzelm
delete commented-out dead code
2011-08-24, by huffman
merged
2011-08-24, by huffman
change some subsection headings to subsubsection
2011-08-24, by huffman
remove unnecessary lemma card_ge1
2011-08-23, by huffman
move connected_real_lemma to the one place it is used
2011-08-23, by huffman
merged
2011-08-24, by wenzelm
make sure that all facts are passed to ATP from minimizer
2011-08-24, by blanchet
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-24, by blanchet
specify timeout for "sledgehammer_tac"
2011-08-24, by blanchet
tuning
2011-08-24, by blanchet
Quotient Package: add mem_rsp, mem_prs, tune proofs.
2011-08-24, by Cezary Kaliszyk
merged
2011-08-23, by huffman
declare euclidean_simps [simp] at the point they are proved;
2011-08-23, by huffman
merged
2011-08-23, by huffman
merged
2011-08-22, by huffman
avoid warnings
2011-08-22, by huffman
comment out dead code to avoid compiler warnings
2011-08-22, by huffman
legacy theorem names
2011-08-22, by huffman
remove duplicate lemma
2011-08-22, by huffman
fixed "hBOOL" of existential variables, and generate more helpers
2011-08-23, by blanchet
don't select facts when using sledgehammer_tac for reconstruction
2011-08-23, by blanchet
don't perform a triviality check if the goal is skipped anyway
2011-08-23, by blanchet
optional reconstructor
2011-08-23, by blanchet
misc tuning and simplification;
2011-08-24, by wenzelm
tuned pri: prefer purging of canceled execution;
2011-08-24, by wenzelm
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24, by wenzelm
clarified Document.Node.clear -- retain header (cf. ML version);
2011-08-24, by wenzelm
clarified norm_header/header_edit -- disallow update of loaded theories;
2011-08-24, by wenzelm
misc tuning and simplification;
2011-08-24, by wenzelm
ignore irrelevant timings;
2011-08-24, by wenzelm
print state only for visible command, to avoid wasting resources for the larger part of the text;
2011-08-24, by wenzelm
early filtering of unchanged perspective;
2011-08-24, by wenzelm
more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
2011-08-24, by wenzelm
update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-24, by wenzelm
tuned;
2011-08-23, by wenzelm
handle potentially more approriate BufferUpdate.LOADED event;
2011-08-23, by wenzelm
special treatment of structure index 1 in Pure, including legacy warning;
2011-08-22, by wenzelm
compile
2011-08-23, by blanchet
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
2011-08-23, by blanchet
beef up "sledgehammer_tac" reconstructor
2011-08-23, by blanchet
clean up Sledgehammer tactic
2011-08-23, by blanchet
fixed document;
2011-08-23, by wenzelm
tuned signature;
2011-08-23, by wenzelm
merged
2011-08-23, by wenzelm
always use TFF if possible
2011-08-23, by blanchet
clearer separator in generated file names
2011-08-23, by blanchet
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23, by blanchet
updated known failures for Z3 3.0 TPTP
2011-08-23, by blanchet
updated Z3 docs
2011-08-23, by blanchet
avoid TFF format with older Vampire versions
2011-08-23, by blanchet
update the Vampire related parts of the documentation
2011-08-23, by blanchet
fixed TFF slicing
2011-08-23, by blanchet
kindly ask Vampire to output axiom names
2011-08-23, by blanchet
added formats to the slice and use TFF for remote Vampire
2011-08-23, by blanchet
tuned specifications, syntax and proofs
2011-08-23, by haftmann
tuned specifications and syntax
2011-08-22, by haftmann
Quotient Package: some infrastructure for lifting inside sets
2011-08-23, by Cezary Kaliszyk
include all encodings in tests, now that the incompleteness of some encodings has been addressed
2011-08-22, by blanchet
change Metis's default settings if type information axioms are generated
2011-08-22, by blanchet
we must tag any type whose ground types intersect a nonmonotonic type
2011-08-22, by blanchet
prefer the lighter, slightly unsound monotonicity-based encodings for Metis
2011-08-22, by blanchet
made reconstruction of type tag equalities "\?x = \?x" reliable
2011-08-22, by blanchet
tuning ATP problem output
2011-08-22, by blanchet
revert guard logic -- make sure that typing information is generated for existentials
2011-08-22, by blanchet
generate tag equations for existential variables
2011-08-22, by blanchet
tuning, plus started implementing tag equation generation for existential variables
2011-08-22, by blanchet
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
2011-08-22, by blanchet
clearer terminology
2011-08-22, by blanchet
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
2011-08-22, by blanchet
removed unused configuration option
2011-08-22, by blanchet
added caching for (in)finiteness checks
2011-08-22, by blanchet
remove needless typing information
2011-08-22, by blanchet
cleaner handling of polymorphic monotonicity inference
2011-08-22, by blanchet
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
2011-08-22, by blanchet
more precise warning
2011-08-22, by blanchet
added option to control soundness of encodings more precisely, for evaluation purposes
2011-08-22, by blanchet
make sound mode more sound (and clean up code)
2011-08-22, by blanchet
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
2011-08-22, by blanchet
gracefully handle empty SPASS problems
2011-08-22, by blanchet
pass sound option to Sledgehammer tactic
2011-08-22, by blanchet
tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-23, by wenzelm
tuned signature;
2011-08-23, by wenzelm
discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
2011-08-23, by wenzelm
some support for toplevel printing wrt. editor perspective (still inactive);
2011-08-23, by wenzelm
propagate editor perspective through document model;
2011-08-23, by wenzelm
some support for editor perspective;
2011-08-22, by wenzelm
discontinued redundant Edit_Command_ID;
2011-08-22, by wenzelm
reduced warnings;
2011-08-22, by wenzelm
tuned message;
2011-08-22, by wenzelm
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