isabelle: Graph

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
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
2012-03-12, by wenzelm
merged
2012-03-11, by wenzelm
renewing Executable_Relation
2012-03-11, by bulwahn
tuned;
2012-03-11, by wenzelm
more direct Name_Space.defined_entry;
2012-03-11, by wenzelm
eliminated old-fashioned 'constrains' element;
2012-03-11, by wenzelm
modernized locale expression, with some fluctuation of arguments;
2012-03-11, by wenzelm
simplified span class in conformance to Scala version;
2012-03-10, by wenzelm
discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
2012-03-10, by wenzelm
merged
2012-03-10, by wenzelm
adding tags to quickcheck's result
2012-03-10, by bulwahn
clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval;
2012-03-10, by wenzelm
eliminated dead code;
2012-03-10, by wenzelm