isabelle: Graph

avoided map_of in def of fun_rep (but still needed for efficient code)
2013-04-18, by nipkow
spelling
2013-04-18, by haftmann
spelling
2013-04-18, by haftmann
tuned
2013-04-17, by nipkow
complete revision: finally got rid of annoying L-predicate
2013-04-17, by nipkow
moved leastness lemma
2013-04-17, by nipkow
proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2);
2013-04-16, by wenzelm
use automatic type coerctions in Sqrt example
2013-04-15, by hoelzl
make SML/NJ happy;
2013-04-15, by wenzelm
not all Nitpick 'constructors' are injective -- careful
2013-04-15, by blanchet
added another definition snipped
2013-04-14, by kleing
actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;
2013-04-12, by wenzelm
modifiers for classical wrappers operate on Proof.context instead of claset;
2013-04-12, by wenzelm
removed historic comments;
2013-04-12, by wenzelm
tuned exceptions -- avoid composing error messages in low-level situations;
2013-04-12, by wenzelm
tuned signature;
2013-04-12, by wenzelm
proper identifiers -- avoid crash of case translations;
2013-04-12, by wenzelm
reduced duplication
2013-04-12, by nipkow
do not add case translation syntax in rep_datatype compatibility mode
2013-04-11, by traytel
run type inference on input to wrap_data
2013-04-11, by traytel
installed case translations in BNF package
2013-04-11, by traytel
tuned
2013-04-11, by nipkow
more antiquotations;
2013-04-10, by wenzelm
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
2013-04-10, by wenzelm
updated keywords;
2013-04-10, by wenzelm
merged
2013-04-10, by wenzelm
merged
2013-04-10, by wenzelm
obsolete -- tools should refer to proper Proof.context;
2013-04-10, by wenzelm
discontinued obsolete ML antiquotation @{claset};
2013-04-10, by wenzelm
added ML antiquotation @{theory_context};
2013-04-10, by wenzelm
more standard module name Axclass (according to file name);
2013-04-10, by wenzelm
made SML/NJ happy
2013-04-10, by traytel
generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
2013-04-10, by hoelzl
NEWS and CONTRIBUTORS
2013-04-10, by traytel
declaration attribute for case combinators
2013-04-10, by traytel
Handle dummy patterns in parse translation rather than check phase
2013-04-09, by berghofe
disallow coercions to interfere with case translations
2013-04-06, by traytel
allow redundant cases in the list comprehension translation
2013-04-05, by traytel
recur in the expression to be matched (do not rely on repetitive execution of a check phase);
2013-04-05, by traytel
tuned whitespace
2013-04-05, by traytel
Use Type.raw_match instead of Sign.typ_match
2013-04-04, by berghofe
special constant to prevent eta-contraction of the check-phase syntax of case translations
2013-04-05, by traytel
separate data used for case translation from the datatype package
2013-01-22, by traytel
case translations performed in a separate check phase (with adjustments by traytel)
2013-01-22, by berghofe
formal proof context for axclass proofs;
2013-04-10, by wenzelm
prefer local context;
2013-04-10, by wenzelm
proper proof context;
2013-04-10, by wenzelm
tuned;
2013-04-10, by wenzelm
merged
2013-04-09, by wenzelm
add command timings (like document command status);
2013-04-09, by wenzelm
tuned signature;
2013-04-09, by wenzelm
public Isabelle_Process.xml_cache (thread-safe);
2013-04-09, by wenzelm
tuned signature;
2013-04-09, by wenzelm
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09, by wenzelm
clarified protocol_message undefinedness;
2013-04-09, by wenzelm
quote by Alan Kay;
2013-04-09, by wenzelm
more accurate documentation;
2013-04-09, by wenzelm
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-09, by wenzelm
more accurate documentation of "(structure)" mixfix;
2013-04-09, by wenzelm
more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
2013-04-09, by wenzelm
tuned comment;
2013-04-09, by wenzelm
just one syntax category "mixfix" -- check structure annotation semantically;
2013-04-09, by wenzelm
tuned message;
2013-04-09, by wenzelm
handle case clashes on Mac file system by encoding goal numbers
2013-04-09, by blanchet
avoid duplicate "tcon_" names
2013-04-09, by blanchet
smoothly handle cyclic graphs
2013-04-09, by blanchet
compile + fixed naming convention
2013-04-09, by blanchet
reverted accidental changes to theory file + updated wrt ML file
2013-04-09, by blanchet
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
2013-04-09, by blanchet
work on CASC LTB ISA exporter
2013-04-09, by blanchet
tuning
2013-04-09, by blanchet
add continuous_on rules for products
2013-04-09, by hoelzl
fixed spelling
2013-04-09, by hoelzl
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-04-09, by hoelzl
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-04-09, by hoelzl
improved printing of exception CTERM (see also d0f0f37ec346);
2013-04-08, by wenzelm
prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
2013-04-08, by wenzelm
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
2013-04-08, by wenzelm
discontinued odd magic number, which was once used for performance measurements;
2013-04-08, by wenzelm
document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);
2013-04-08, by wenzelm
merged
2013-04-08, by wenzelm
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
2013-04-08, by wenzelm
try to preserve original linearization
2013-04-08, by blanchet
use somewhat lighter encoding
2013-04-08, by blanchet
robustness w.r.t. unknown arguments
2013-04-08, by blanchet
cleaned
2013-04-07, by nipkow
cleaned
2013-04-07, by nipkow
tuned
2013-04-06, by nipkow
tuned signature -- agree with markup terminology;
2013-04-05, by wenzelm
unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-04-05, by wenzelm
tuned document
2013-04-05, by nipkow
tuned
2013-04-05, by nipkow
sup on multisets
2013-04-04, by haftmann
convenient induction rule
2013-04-04, by haftmann
tuned README -- less buzzwords;
2013-04-04, by wenzelm
more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);
2013-04-04, by wenzelm
added missing file;
2013-04-04, by wenzelm
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
2013-04-04, by wenzelm
tuned signature -- concentrate GUI tools;
2013-04-04, by wenzelm
tuned signature -- concentrate GUI tools;
2013-04-04, by wenzelm
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
2013-04-04, by wenzelm
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
2013-04-04, by wenzelm
tuned imports;
2013-04-04, by wenzelm
added var_position in analogy to longid_position, for typing reports on input;
2013-04-04, by wenzelm
removed unnerving (esp in jedit) and pointless warning
2013-04-04, by nipkow
tuned
2013-04-04, by nipkow
merged
2013-04-03, by wenzelm
tuned;
2013-04-03, by wenzelm
recover implicit thread position for status messages (cf. eca8acb42e4a);
2013-04-03, by wenzelm
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-04-03, by wenzelm
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
2013-04-03, by wenzelm
updated comment to 46b90bbc370d;
2013-04-03, by wenzelm
recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);
2013-04-03, by wenzelm
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
2013-04-03, by wenzelm
tuned output -- less bullets;
2013-04-03, by wenzelm
default implementation of multisets by list with reasonable coverage of operations on multisets
2013-04-03, by haftmann
optionalized very specific code setup for multisets
2013-04-03, by haftmann
generalized lemma fold_image thanks to Peter Lammich
2013-04-03, by haftmann
tuned;
2013-04-02, by wenzelm
NEWS for 635562bc14ef;
2013-04-02, by wenzelm