isabelle: Graph

more abstract heading level;
2012-03-16, by wenzelm
less redundant data;
2012-03-16, by wenzelm
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
2012-03-16, by wenzelm
merged
2012-03-16, by wenzelm
ZF news
2012-03-16, by paulson
merged
2012-03-16, by paulson
Structured transfinite induction proofs
2012-03-16, by paulson
make more word theorems respect int/bin distinction
2012-03-16, by huffman
outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16, by wenzelm
refute_params are given in *this* theory;
2012-03-16, by wenzelm
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2012-03-16, by wenzelm
define keywords early when processing the theory header, before running the body commands;
2012-03-16, by wenzelm
clarified Keyword.is_keyword: union of minor and major;
2012-03-16, by wenzelm
Isabelle/jEdit supports user-defined Isar commands within the running session;
2012-03-15, by wenzelm
merged
2012-03-15, by wenzelm
beautification and structured proofs
2012-03-15, by paulson
replacing ":" by "\<in>"
2012-03-15, by paulson
Rewrote some induction proofs to be structured
2012-03-15, by paulson
more precise TPTP keywords and dependencies;
2012-03-15, by wenzelm
declare command keywords via theory header, including strict checking outside Pure;
2012-03-15, by wenzelm
prefer formally checked @{keyword} parser;
2012-03-15, by wenzelm
added ML antiquotation @{keyword};
2012-03-15, by wenzelm
declare minor keywords via theory header;
2012-03-15, by wenzelm
more explicit header_edits before main text_edits;
2012-03-15, by wenzelm
declare keywords as side-effect of header edit;
2012-03-15, by wenzelm
more recent recent_syntax, e.g. relevant for document rendering during startup;
2012-03-15, by wenzelm
clarified syntax of prospective keywords;
2012-03-15, by wenzelm
basic support for outer syntax keywords in theory header;
2012-03-15, by wenzelm
maintain Version.syntax within document state;
2012-03-15, by wenzelm
explicit Outer_Syntax.Decl;
2012-03-15, by wenzelm
allow multiple 'keywords' as in 'fixes';
2012-03-15, by wenzelm
some support for outer syntax keyword declarations within theory header;
2012-03-15, by wenzelm
merged
2012-03-14, by wenzelm
merged
2012-03-14, by paulson
structured case and induct rules
2012-03-14, by paulson
rudimentary documentation test
2012-03-14, by haftmann
doc-src build option (for emerging mira configuration)
2012-03-14, by haftmann
corrected fragile proof; tuned semicolons
2012-03-14, by haftmann
rudimentary distribution build configuration
2012-03-14, by haftmann
support for non-HTTP repository locations (important for mira); quasi-hardwired repository name
2012-03-14, by haftmann
corrected slip
2012-03-14, by haftmann
merged
2012-03-14, by paulson
rationalising the induction rule trans_induct3
2012-03-14, by paulson
allow modification of REPOS_NAME and REPOS from outside
2012-03-14, by haftmann
locale expressions without source positions;
2012-03-14, by wenzelm
tuned;
2012-03-14, by wenzelm
tuned messages;
2012-03-14, by wenzelm
source positions for locale and class expressions;
2012-03-14, by wenzelm
some proof indentation;
2012-03-14, by wenzelm
more explicit indication of swing thread context;
2012-03-14, by wenzelm
more indentation;
2012-03-14, by wenzelm
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
2012-03-14, by wenzelm
eliminated obsolete sanitize_name;
2012-03-14, by wenzelm
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
2012-03-14, by wenzelm
more parallel inductive_cases;
2012-03-14, by wenzelm
misc tuning;
2012-03-14, by wenzelm
updated to jedit_build-20120313 with jedit-4.5.0;
2012-03-13, by wenzelm
tuned context specifications and proofs;
2012-03-13, by wenzelm
tuned proofs;
2012-03-13, by wenzelm
clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-13, by wenzelm
more explicit indication of def names;
2012-03-13, by wenzelm
merged
2012-03-13, by paulson
Structured proofs concerning the square of an infinite cardinal
2012-03-13, by paulson
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
2012-03-13, by wenzelm
prefer abs_def over def_raw;
2012-03-13, by wenzelm
prefer abs_def over def_raw;
2012-03-13, by wenzelm
improved attribute "abs_def" to handle object-equality as well;
2012-03-13, by wenzelm
merged
2012-03-13, by wenzelm
More structured proofs about cardinal arithmetic
2012-03-13, by paulson
tuned proofs;
2012-03-13, by wenzelm
refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
2012-03-13, by wenzelm
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-03-13, by wenzelm
proper printing of empty binding (again, cf. 93f6f24010c2);
2012-03-13, by wenzelm
tuned;
2012-03-13, by wenzelm
tuned strip_alls;
2012-03-13, by wenzelm
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
2012-03-13, by wenzelm
some grouping of Par_List operations, to adjust granularity;
2012-03-12, by wenzelm
Par_List.map is already smart;
2012-03-12, by wenzelm
some support for grouped list operations;
2012-03-12, by wenzelm
merged;
2012-03-12, by wenzelm
merged
2012-03-12, by noschinl
NEWS
2012-03-12, by noschinl
use eventually_elim method
2012-03-12, by noschinl
add eventually_elim method
2012-03-12, by noschinl
merged
2012-03-12, by noschinl
tuned proofs
2012-03-12, by noschinl
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
2012-03-12, by noschinl
tuned simpset
2012-03-12, by noschinl
activate_notes in parallel -- to speedup main operation of locale interpretation;
2012-03-12, by wenzelm
refined activate_notes: simultaneous transformation before activation;
2012-03-12, by wenzelm
tuned headers;
2012-03-12, by wenzelm
merged
2012-03-12, by paulson
Structured proofs in ZF
2012-03-12, by paulson
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
2012-03-12, by wenzelm
updated polyml/build option to prefer included libffi;
2012-03-12, by wenzelm
tuned signature;
2012-03-12, by wenzelm