isabelle: Graph

Added material by David Trachtenherz
2011-02-26, by nipkow
corrected HOLCF dependency on Nat_Infinity
2011-02-26, by nipkow
got rid of lemma upper_bound_finite_set
2011-02-25, by nipkow
merged
2011-02-25, by nipkow
Some cleaning up
2011-02-25, by nipkow
updated generated files
2011-02-25, by krauss
fixed manual (rule no longer exists)
2011-02-25, by krauss
removed support for tail-recursion from function package (now implemented by partial_function)
2011-02-25, by krauss
reactivate time measurement (partly reverting c27b0b37041a);
2011-02-25, by krauss
generalize find_theorems filters to work on raw propositions, too
2011-02-25, by krauss
merged
2011-02-25, by nipkow
added simp lemma nth_Cons_pos to List
2011-02-25, by nipkow
Refactor find_theorems to provide a more general filter_facts method
2011-02-25, by noschinl
removed dead code/unused exports/speculative generality
2011-02-25, by krauss
recdef -> fun(ction)
2011-02-24, by krauss
removed unused lemma
2011-02-24, by krauss
recdef -> fun(ction);
2011-02-24, by krauss
eliminated clones of List.upto
2011-02-24, by krauss
fix non-exhaustive pattern match in find_theorems
2011-02-23, by noschinl
merged
2011-02-23, by hoelzl
add lemma KL_divergence_vimage, mutual_information_generic
2011-02-23, by hoelzl
add lemma RN_deriv_vimage
2011-02-23, by hoelzl
use measure_preserving in ..._vimage lemmas
2011-02-23, by hoelzl
log is borel measurable
2011-02-23, by hoelzl
add name continuous_isCont to unnamed lemma
2011-02-22, by hoelzl
add example for case_product usage
2011-02-23, by noschinl
setup case_product attribute in HOL and FOL
2011-02-23, by noschinl
introduce attribute case_prod for combining case rules
2010-12-08, by noschinl
merged
2011-02-23, by blanchet
remove confusing message
2011-02-23, by blanchet
eliminated remdps in favor of List.remdups
2011-02-23, by krauss
recdef -> fun
2011-02-23, by krauss
recdef -> fun
2011-02-23, by krauss
updated generated file;
2011-02-22, by wenzelm
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
2011-02-22, by wenzelm
modernized specifications;
2011-02-22, by wenzelm
dropped obsolete FIXMEs
2011-02-22, by krauss
merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
2011-02-21, by wenzelm
eliminated global prems
2011-02-21, by krauss
modernized specification; curried
2011-02-21, by krauss
recdef -> fun; curried
2011-02-21, by krauss
recdef -> fun; curried
2011-02-21, by krauss
strengthened polymul.induct
2011-02-21, by krauss
dropped stupid name
2011-02-21, by krauss
removed duplicate declarations
2011-02-21, by krauss
recdef -> function
2011-02-21, by krauss
tuned proofs -- eliminated prems;
2011-02-21, by wenzelm
merged
2011-02-21, by blanchet
adjust example
2011-02-21, by blanchet
document new "preconstr" option
2011-02-21, by blanchet
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21, by blanchet
more work on "fix_datatype_vals"
2011-02-21, by blanchet
first steps in implementing "fix_datatype_vals" optimization
2011-02-21, by blanchet
better fudge factors for CVC3 and Yices based on Judgment Day
2011-02-21, by blanchet
exit code 127 can mean many things -- not just (and probably not) Perl missing
2011-02-21, by blanchet
modernized specifications;
2011-02-21, by wenzelm
rename Nitpick's (internal) auxiliary lemmas
2011-02-21, by blanchet
updated docs w.r.t. "nitpick_unfold" attribute
2011-02-21, by blanchet
improve optimization
2011-02-21, by blanchet
updated docs
2011-02-21, by blanchet
tweaked Nitpick based on C++ memory model example
2011-02-21, by blanchet
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-02-21, by blanchet
always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-02-21, by blanchet
give more weight to Frees than to Consts in relevance filter
2011-02-21, by blanchet
don't distinguish between "fixes" and other free variables -- this confuses users
2011-02-21, by blanchet
added a timeout around SMT preprocessing (notably monomorphization)
2011-02-21, by blanchet
comments to find fudge factors easily
2011-02-21, by blanchet
added test cases with quantifier occurring in first-order term positions
2011-02-21, by boehmes
wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
2011-02-21, by boehmes
dropped redundancy
2011-02-19, by haftmann
merged
2011-02-19, by haftmann
added is_IAbs; tuned brackets and comments
2011-02-17, by haftmann
more idiomatic printing of let cascades and type variable constraints
2011-02-17, by haftmann
merged
2011-02-18, by wenzelm
modernized specifications;
2011-02-18, by wenzelm
modernized specifications;
2011-02-18, by wenzelm
more precise headers;
2011-02-18, by wenzelm
less verbose tracing;
2011-02-18, by wenzelm
standardized headers;
2011-02-18, by wenzelm
modernized specifications;
2011-02-18, by wenzelm
gracious timeout in "blocking" mode
2011-02-18, by blanchet
make Nitpick's timeout mechanism somewhat more reliable/friendly;
2011-02-18, by blanchet
better fudge factors for Sledgehammer
2011-02-18, by blanchet
adjust fudge factors
2011-02-18, by blanchet
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
2011-02-18, by blanchet
export more functionality of Sledgehammer to applications (for experiments)
2011-02-17, by blanchet
export useful function (needed in a Sledgehammer-related experiment)
2011-02-16, by blanchet
make experimental "Z3 ATP" work on Linux as well
2011-02-15, by blanchet
adjusted fudge factors (based on Judgment Day runs)
2011-02-15, by blanchet
generalized termination lemmas
2011-02-14, by nipkow
strengthened induction rule;
2011-02-14, by krauss
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
2011-02-14, by boehmes
more explicit errors to inform users about problems related to SMT solvers;
2011-02-14, by boehmes
more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1;
2011-02-13, by wenzelm
eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;
2011-02-13, by wenzelm
tuned;
2011-02-13, by wenzelm
more pretty set comprehension sugar
2011-02-13, by nipkow
merged
2011-02-11, by bulwahn
adjusting HOL-Mutabelle to changes in quickcheck
2011-02-11, by bulwahn
quickcheck can be invoked with its internal timelimit or without
2011-02-11, by bulwahn
quickcheck invokes TimeLimit.timeLimit only in one separate function
2011-02-11, by bulwahn
added option to Mirabelle Sledgehammer
2011-02-11, by blanchet
merged
2011-02-10, by haftmann
reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
2011-02-10, by haftmann
tuning
2011-02-10, by blanchet
fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)
2011-02-10, by blanchet
fix path to etc/settings and etc/components in doc
2011-02-10, by blanchet
run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
2011-02-10, by blanchet
remove pointless clutter
2011-02-10, by blanchet
make minimizer verbose
2011-02-10, by blanchet
tuning
2011-02-09, by blanchet
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2011-02-09, by blanchet
renamed field
2011-02-09, by blanchet
added "Z3 as an ATP" support to Sledgehammer locally
2011-02-09, by blanchet
remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files
2011-02-09, by blanchet
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
2011-02-09, by blanchet
tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;
2011-02-09, by wenzelm
merged
2011-02-09, by bulwahn
changing auto-quickcheck to be considered a non-interactive invocation of quickcheck
2011-02-08, by bulwahn
discontinued obsolete lib/scripts/polyml-platform;
2011-02-08, by wenzelm
clarified comment -- ancienct PG 3.7.x is still in use;
2011-02-08, by wenzelm
discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
2011-02-08, by wenzelm
prefer polyml-5.2.1 over odd polyml-5.3.0-old;
2011-02-08, by wenzelm
some shuffling of isatest settings, to ensure coverage of polyml-5.2.1, polyml-5.3.0, polyml-5.4.0, polyml-5.4.1 (SVN), smlnj/110.72;
2011-02-08, by wenzelm
reverted slightly odd eb5900951702: isatest-doc should work again due to 4b08499b3db1 (polyml-5.3.0 supports proper TimeLimit, as required for HOL-Nitpick-Examples);
2011-02-08, by wenzelm
merged
2011-02-08, by wenzelm
available_provers ~> supported_provers (for clarity)
2011-02-08, by blanchet
sort E weights
2011-02-08, by blanchet
added support for bleeding-edge E weighting function "SymOffsetsWeight"
2011-02-08, by blanchet
transformed lie into truth
2011-02-08, by blanchet
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite
2011-02-08, by blanchet
improving sum type and option type term constructions for correct presentation in Smallcheck
2011-02-08, by bulwahn
Explicitly build HOLCF and ZF images. They are not part of the release any more.
2011-02-08, by kleing
added termination lemmas
2011-02-08, by nipkow
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
2011-02-07, by bulwahn
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
2011-02-08, by wenzelm
tuned headers;
2011-02-08, by wenzelm
updated to polyml-5.3.0, which is presently known as the most robust version;
2011-02-08, by wenzelm
explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
2011-02-08, by wenzelm
always test/clear Multithreading.interrupted, indepently of thread attributes;
2011-02-08, by wenzelm
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
2011-02-08, by wenzelm
more robust TimeLimit: make double sure that watchdog has terminated and interrupts received during uninterruptible state are propagated (NB: Thread.testInterrupt requires InterruptSynch in Poly/ML 5.4.0 or earlier);
2011-02-07, by wenzelm
more tracing information via Par_List.map_name;
2011-02-05, by wenzelm
clarified bootstrapping of structure TimeLimit;
2011-02-05, by wenzelm
more scalable collections of tasks, notably for totality of known group members;
2011-02-04, by wenzelm
tuned signature;
2011-02-04, by wenzelm
merged
2011-02-04, by wenzelm
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
2011-02-04, by hoelzl
add auto support for AE_mp
2011-02-04, by hoelzl
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
2011-02-04, by hoelzl
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
2011-02-04, by wenzelm
Task_Queue.update_timing: more precise treatment of interruptibility;
2011-02-04, by wenzelm
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
2011-02-04, by wenzelm
thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
2011-02-03, by wenzelm
tuned comments;
2011-02-03, by wenzelm
clarified Proofterm.proofs_enabled;
2011-02-03, by wenzelm
explicit is better than implicit;
2011-02-03, by wenzelm
tuned odd conditional expression;
2011-02-02, by wenzelm
eliminated slightly odd abstract type Task_Queue.deps;
2011-02-02, by wenzelm
merged
2011-02-02, by wenzelm
Introduction of metis calls and other cosmetic modifications.
2011-02-02, by paulson
merged
2011-02-02, by boehmes
avoid ML structure aliases (especially single-letter abbreviations)
2011-02-02, by boehmes
making the bash script swipl_version closer to Isabelle's conventional bash scripts
2011-02-02, by bulwahn
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
2011-02-02, by hoelzl
merged
2011-02-02, by bulwahn
scala serializer adds parentheses around function literals
2011-02-02, by bulwahn
made SML/NJ happy
2011-02-02, by krauss
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
2011-02-01, by krauss
refined Task_Queue.dequeue_deps (more incremental);
2011-02-02, by wenzelm
maintain Task_Queue.group within Task_Queue.task;
2011-02-02, by wenzelm
tuned comment;
2011-02-02, by wenzelm
Future.join_results: discontinued post-hoc recording of dynamic dependencies;
2011-02-02, by wenzelm
more informative task timing: some dependency tracking;
2011-02-01, by wenzelm
refined task timing: joining vs. waiting;
2011-02-01, by wenzelm
simplified trace;
2011-02-01, by wenzelm
more specific Goal.fork_name;
2011-01-31, by wenzelm
name "passive" tasks (practically lazy values);
2011-01-31, by wenzelm
tuned trivial cases;
2011-01-31, by wenzelm
tuned signature;
2011-01-31, by wenzelm
support named tasks, for improved tracing;
2011-01-31, by wenzelm
more direct Future.bulk, which potentially reduces overhead for Par_List;
2011-01-31, by wenzelm
tuned isatest settings;
2011-01-31, by wenzelm
added basic task timing;
2011-01-31, by wenzelm
some notes on Cygwin;
2011-01-31, by wenzelm
more platform hints;
2011-01-31, by wenzelm
merged
2011-01-31, by wenzelm
tuned;
2011-01-31, by wenzelm
back to post-release mode;
2011-01-31, by wenzelm
removed obsolete test tags;
2011-01-30, by wenzelm
removed Florian's email from isatest (bounces)
2011-01-28, by kleing
merged
2011-01-25, by hoelzl
use pre-image measure, instead of image
2011-01-24, by hoelzl
use AE_mp in AE_conjI proof
2011-01-21, by hoelzl
tuned proof
2011-01-19, by hoelzl
merged
2011-01-21, by haftmann
moved theorem
2011-01-21, by haftmann
restructured theory;
2011-01-21, by haftmann
merged
2011-01-19, by hoelzl
Gauge measure removed
2011-01-18, by hoelzl
merged
2011-01-18, by haftmann
report mutabelle log in mira configuration
2011-01-18, by haftmann
back to post-release mode;
2011-01-17, by wenzelm
delete .elc files unconditionally -- they cause too many incompatibilities;
2011-01-30, by wenzelm
Added tag Isabelle2011 for changeset 6d736d983d5c
2011-01-30, by wenzelm
clarified example settings for Proof General; Isabelle2011
2011-01-30, by wenzelm
adhoc patches relative to ProofGeneral-4.1pre101216, which has setprefs working;
2011-01-28, by wenzelm
more precise stats;
2011-01-28, by wenzelm
some adhoc patches for ProofGeneral-4.1pre110112;
2011-01-28, by wenzelm
enforce STIXGeneral, which is preferred by PG 4.1;
2011-01-28, by wenzelm
default UTF-8 locale, to work with funny base directory (e.g. Chinese);
2011-01-28, by wenzelm
enforce fonts;
2011-01-28, by wenzelm
added option -f FONT;
2011-01-27, by wenzelm
Proof General 4.x interface wrapper;
2011-01-27, by wenzelm
old Proof General patches;
2011-01-27, by wenzelm
Added tag isa2011-test3 for changeset 55a45051b220
2011-01-27, by wenzelm
Tuned definition of sdiv.
2011-01-27, by berghofe
CRITICAL markup for critical poking with unsynchronized references;
2011-01-27, by wenzelm
Replaced smod by standard mod operator to reflect actual behaviour
2011-01-26, by berghofe
cancel document execution before editing, to improve reactivity on systems with few cores;
2011-01-27, by wenzelm
tuned isatest settings (for Poly/ML SVN 1278);
2011-01-25, by wenzelm
merged
2011-01-25, by wenzelm
do not restore old files on startup, which is potentially slow due to automatic rechecking;
2011-01-25, by wenzelm
singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
2011-01-25, by wenzelm
workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
2011-01-25, by wenzelm
improved README -- Isabelle symbols and fonts;
2011-01-24, by wenzelm
delete compiled .elc files to improve portability on Linux, notably for GNU Emacs 23.1.x instead of 23.2.x;
2011-01-24, by wenzelm
do not overwrite proof-shell-quit-timeout by default (final PG 4.1 supposedly gets it right);
2011-01-23, by wenzelm
Added tag isa2011-test2 for changeset 237328506a42
2011-01-23, by wenzelm
Documented unused_thms
2011-01-23, by berghofe
JVM/Windows: more robust treatment of unicode in file names;
2011-01-21, by wenzelm
java/scala: default to UTF-8;
2011-01-21, by wenzelm
updated Named_Target.init;
2011-01-21, by wenzelm
made SML/NJ happy;
2011-01-21, by wenzelm
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
2011-01-20, by wenzelm
fixing list_to_set_comprehension simproc
2011-01-19, by bulwahn
more release checks;
2011-01-19, by wenzelm
potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
2011-01-19, by wenzelm
clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;
2011-01-19, by wenzelm
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
2011-01-19, by wenzelm
merged
2011-01-19, by wenzelm
tuned;
2011-01-19, by wenzelm
Cygwin: back to ProofGeneral-3.7.1.1 with XEmacs, since PG 4.x with GNU Emacs 23 is painfully slow;
2011-01-19, by wenzelm
isabelle jedit as alternative;
2011-01-18, by wenzelm
Apple's way of locating java;
2011-01-18, by wenzelm
more notes on final release stage;
2011-01-18, by wenzelm
makedist: refer to isabelle-release;
2011-01-17, by wenzelm
Added tag isa2011-test1 for changeset 7d035da21e9c
2011-01-17, by wenzelm
tuned;
2011-01-17, by wenzelm
some announcement;
2011-01-17, by wenzelm
tuned;
2011-01-17, by wenzelm
merged
2011-01-17, by wenzelm
made Z3 the default SMT solver again
2011-01-17, by boehmes
some notes on final release stage;
2011-01-17, by wenzelm
isatest: run at-poly on macbroy28 for slightly more robust isatest-doc;
2011-01-17, by wenzelm
keep Proof General 4.0 and 3.7.1.1 for now;
2011-01-17, by wenzelm
tuned;
2011-01-16, by wenzelm
misc updates for release;
2011-01-16, by wenzelm
tuned;
2011-01-16, by wenzelm
misc tuning for release;
2011-01-16, by wenzelm
merged
2011-01-16, by wenzelm
Tuned show_status
2011-01-16, by berghofe
proper type variables with sorts;
2011-01-16, by wenzelm
non-executable sources;
2011-01-16, by wenzelm
tuned headers;
2011-01-16, by wenzelm
tuned;
2011-01-16, by wenzelm
type_synonym;
2011-01-16, by wenzelm
more standard command descriptions;
2011-01-16, by wenzelm
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-16, by wenzelm
Replaced ad-hoc advance function by Position.advance
2011-01-15, by berghofe
merged
2011-01-15, by wenzelm
experimental variant of interpretation with simultaneous definitions, plus example
2011-01-15, by haftmann
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2011-01-15, by wenzelm
link HOL-Proofs/index.html, which is not reachable from regular HOL/index.html;
2011-01-15, by wenzelm
type_synonym;
2011-01-15, by wenzelm
recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e;
2011-01-15, by wenzelm
export Record.get_hierarchy -- external tools typically need this information;
2011-01-15, by wenzelm
tuned;
2011-01-15, by wenzelm
removed unreferenced identifiers;
2011-01-15, by wenzelm
global "prems" is legacy feature;
2011-01-15, by wenzelm
misc updates for release;
2011-01-15, by wenzelm
merged;
2011-01-15, by wenzelm
misc tuning for release;
2011-01-15, by wenzelm
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
2011-01-15, by boehmes
Also added SPARK to test and clean targets.
2011-01-15, by berghofe
merged
2011-01-15, by berghofe
Added entry for HOL-SPARK
2011-01-15, by berghofe
Added HOL-SPARK and removed old_primrec.ML
2011-01-15, by berghofe
unused_thms no longer compares propositions, since this is no longer needed
2011-01-15, by berghofe
Include HOL-SPARK keywords
2011-01-15, by berghofe
Include HOL-SPARK
2011-01-15, by berghofe
Finally removed old primrec package, since Primrec.add_primrec_global
2011-01-15, by berghofe
Added new SPARK verification environment.
2011-01-15, by berghofe
remove presently unused Isabelle application for official releases;
2011-01-15, by wenzelm
hardwired default for proof-shell-quit-timeout (PG 4.1 provides rather low value);
2011-01-15, by wenzelm
treat HOLCF as HOL library session, not as "logic";
2011-01-15, by wenzelm
increased startup-timeout to accommodate slow systems (especially Windows/Cygwin);
2011-01-15, by wenzelm
bundle main HOL image only, to save about 300 MB disk space;
2011-01-14, by wenzelm
updated for release;
2011-01-14, by wenzelm
adjusted mira configuration
2011-01-14, by haftmann
merged
2011-01-14, by wenzelm
global "prems" is legacy feature;
2011-01-14, by wenzelm
tuned markup;
2011-01-14, by wenzelm
eliminated global prems;
2011-01-14, by wenzelm
more precise import;
2011-01-14, by wenzelm
Thy_Load.begin_theory: maintain source specification of imports;
2011-01-14, by wenzelm
merged
2011-01-14, by hoelzl
integral on lebesgue measure is extension of integral on borel measure
2011-01-14, by hoelzl
tuned formalization of subalgebra
2011-01-14, by hoelzl
introduced integral syntax
2011-01-14, by hoelzl
tuned theorem order
2011-01-14, by hoelzl
configuration file for mira
2011-01-14, by haftmann
eliminated global prems;
2011-01-13, by wenzelm
more precise pretty printing -- to accomodate Scala message layout;
2011-01-13, by wenzelm
less verbosity -- avoid slightly odd tracing information on warning channel;
2011-01-13, by wenzelm
updated Isabelle/jEdit limitations and workarounds;
2011-01-13, by wenzelm
full theory path enables loading parents via master directory and keeps files strictly separate;
2011-01-13, by wenzelm
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-13, by wenzelm
clarified split_thy_path;
2011-01-13, by wenzelm
less verbosity;
2011-01-13, by wenzelm
proper 'domain' class instance for 'a defl, with deflation combinator
2011-01-12, by huffman
documented Option.bind
2011-01-12, by krauss
CONTRIBUTORS
2011-01-12, by krauss
updated keywords;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
updated to ProofGeneral-4.x;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
tuned proof;
2011-01-12, by wenzelm
eliminated global prems;
2011-01-12, by wenzelm
compile;
2011-01-12, by wenzelm
more FIXMEs concerning bad catch-all exception handlers;
2011-01-12, by wenzelm
eliminated obsolete print_sign_exn_unit;
2011-01-12, by wenzelm
reraise interrupts as usual;
2011-01-12, by wenzelm
avoid catch-all exception handler, presumably TERM was meant here;
2011-01-12, by wenzelm
disabled experimental treatment of replacement text for now, which leads to odd spacing and strange effects on non-poppler viewers;
2011-01-12, by wenzelm
observe line length limit;
2011-01-12, by wenzelm
smart_string_of_real: print integer values without fractional part;
2011-01-12, by wenzelm
tuned (cf. 2fe62d602681);
2011-01-11, by wenzelm
added dist/jedit symlink for convenience;
2011-01-11, by wenzelm
record versions of both jEdit and Isabelle;
2011-01-11, by wenzelm
updated to Isabelle2011;
2011-01-11, by wenzelm
isabelle version -i;
2011-01-11, by wenzelm
NEWS
2011-01-11, by haftmann
NEWS
2011-01-11, by bulwahn
eliminated duplication
2011-01-11, by krauss
merged
2011-01-11, by wenzelm
tuned text
2011-01-11, by haftmann
"enriched_type" replaces less specific "type_lifting"
2011-01-11, by haftmann
clarified notion Position.is_reported;
2011-01-11, by wenzelm
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
2011-01-10, by wenzelm
refined ML_Lex.flatten: ensure proper separation of tokens;
2011-01-10, by wenzelm
ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
2011-01-10, by wenzelm
use just one data slot to VC-related information
2011-01-10, by boehmes
be more precise: also merge option values
2011-01-10, by boehmes
only print warning in a visible context (previously, the warning was printed more than once)
2011-01-10, by boehmes
dropped superfluous error message
2011-01-10, by boehmes
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
2011-01-10, by krauss
updated for polyml-5.4.0;
2011-01-10, by wenzelm
made SML/NJ happy;
2011-01-10, by wenzelm
added merge_options convenience;
2011-01-10, by wenzelm
tuned string_of_int to avoid allocation for small integers;
2011-01-10, by wenzelm
eliminated Int.toString;
2011-01-10, by wenzelm
eliminated obsolete LargeInt -- Int is unbounded;
2011-01-10, by wenzelm
standardized split_last/last_elem towards List.last;
2011-01-10, by wenzelm
removing dead code; tuned
2011-01-10, by bulwahn
made SML/NJ happy
2011-01-10, by bulwahn
reverted 08240feb69c7 -- breaks positions of reports;
2011-01-09, by wenzelm
ML_trace: observe context visibility flag (import for Latex mode, for example);
2011-01-09, by wenzelm
more direct treatment of Position.end_offset;
2011-01-09, by wenzelm
discontinued unused end_line, end_column;
2011-01-09, by wenzelm
more scalable HTML.output_width;
2011-01-09, by wenzelm
refined comment (again);
2011-01-09, by wenzelm
merged
2011-01-08, by huffman
use proper syntactic types for 'syntax' commands
2011-01-08, by huffman
make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion
2011-01-08, by huffman
use full path for library imports
2011-01-08, by huffman
types -> type_synonym
2011-01-08, by huffman
updated NEOS_SERVER, which is now provided via settings;
2011-01-08, by wenzelm
renamed Sum_Of_Squares to Sum_of_Squares;
2011-01-08, by wenzelm
Ord_List.merge convenience;
2011-01-08, by wenzelm
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2011-01-08, by wenzelm
modernized structure Prop_Logic;
2011-01-08, by wenzelm
added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);
2011-01-08, by wenzelm