isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

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
tuned;
2011-01-08, by wenzelm
tuned;
2011-01-08, by wenzelm
tuned headers;
2011-01-08, by wenzelm
merged
2011-01-07, by wenzelm
adding example theory for list comprehension to set comprehension simproc
2011-01-07, by bulwahn
adopting proofs due to new list comprehension to set comprehension simproc
2011-01-07, by bulwahn
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
2011-01-07, by bulwahn
tuned text
2011-01-07, by boehmes
merged
2011-01-07, by bulwahn
removing obselete Id comments from HOL/ex theories
2011-01-07, by bulwahn
added hints about licensing restrictions and how to enable Z3
2011-01-07, by boehmes
tuned
2011-01-07, by boehmes
eliminated hard tabs;
2011-01-07, by wenzelm
allow spaces in $SPASS_HOME value;
2011-01-07, by wenzelm
tuned;
2011-01-07, by wenzelm
eliminated alias;
2011-01-07, by wenzelm
do not open ML structures;
2011-01-07, by wenzelm
more standard package setup;
2011-01-07, by wenzelm
do not open ML structures;
2011-01-07, by wenzelm
updated scala;
2011-01-07, by wenzelm
do not open ML structures;
2011-01-07, by wenzelm
do not open Codegen;
2011-01-07, by wenzelm
tuned whitespace, indentation, comments;
2011-01-07, by wenzelm
updated for release;
2011-01-07, by wenzelm
tuned;
2011-01-07, by wenzelm
more precise parentheses and indentation;
2011-01-07, by wenzelm
comments;
2011-01-07, by wenzelm
updated for 2011;
2011-01-07, by wenzelm
shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
2011-01-07, by boehmes
tuned NEWS
2011-01-07, by krauss
avoid ML structure aliases (especially single-letter abbreviations)
2011-01-07, by boehmes
made SML/NJ happy
2011-01-07, by boehmes
rename constant u_defl to u_liftdefl;
2011-01-06, by huffman
rename constant pdefl to liftdefl_of
2011-01-06, by huffman
Diagnostic command to show locale dependencies.
2011-01-06, by ballarin
Documentation for 'interpret' and 'sublocale' with mixins.
2011-01-06, by ballarin
Abelian group facts obtained from group facts via interpretation (sublocale).
2011-01-06, by ballarin
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
2011-01-06, by boehmes
remove various lemmas redundant with lub_eq_bottom_iff
2011-01-04, by huffman
change some lemma names containing 'UU' to 'bottom'
2011-01-04, by huffman
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
2011-01-04, by huffman
merged
2011-01-03, by boehmes