isabelle: Graph

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

proper Envir.norm_type for result of Type.raw_unifys;
2014-11-08, by wenzelm
avoid slow metis proof;
2014-11-08, by wenzelm
proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
2014-11-08, by wenzelm
tuned;
2014-11-08, by wenzelm
updated some sledgehammer proofs -- much faster;
2014-11-08, by wenzelm
updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);
2014-11-08, by wenzelm
recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
2014-11-08, by wenzelm
more direct type equality;
2014-11-08, by wenzelm
reverted commit accident from 994fe0ba8335
2014-11-08, by haftmann
less space-wasting serialization setup: highest cell of array has been unused so far
2014-11-08, by haftmann
tuned outline;
2014-11-07, by wenzelm
tuned syntax -- separate tokens;
2014-11-07, by wenzelm
eliminated pointless check -- command definitions are subject to theory context;
2014-11-07, by wenzelm
merged
2014-11-07, by wenzelm
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
2014-11-07, by wenzelm
tuned markup;
2014-11-07, by wenzelm
tuned;
2014-11-07, by wenzelm
clarified keyword categories;
2014-11-07, by wenzelm
tuned signature;
2014-11-07, by wenzelm
tuned;
2014-11-07, by wenzelm
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-07, by wenzelm
proper import for command 'permanent_interpretation';
2014-11-07, by wenzelm
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
2014-11-07, by wenzelm
more accurate keywords;
2014-11-07, by wenzelm
tuned signature;
2014-11-06, by wenzelm
more explicit Keyword.keywords;
2014-11-06, by wenzelm
proper Keyword.keywords (cf. 82a71046dce8);
2014-11-06, by wenzelm
prefer explicit Keyword.keywords (cf. 82a71046dce8);
2014-11-06, by wenzelm
tuned signature;
2014-11-06, by wenzelm
prefer explicit Keyword.keywords;
2014-11-06, by wenzelm
simplified keyword kinds;
2014-11-06, by wenzelm
Tidying up. Removing unnecessary conditions from some theorems.
2014-11-07, by paulson
more complete fp_sugars for sum and prod;
2014-11-07, by traytel
document '*_transfer' attribute
2014-11-07, by desharna
document 'size_neq'
2014-11-07, by desharna
generate 'size_neq' for datatypes
2014-11-07, by desharna
fix 'unfla' function
2014-11-06, by desharna
proper oriented equivalence of dvd predicate and mod
2014-11-05, by haftmann
merged
2014-11-05, by wenzelm
more symbols;
2014-11-05, by wenzelm
tuned signature;
2014-11-05, by wenzelm
more uniform header_keywords in ML/Scala;
2014-11-05, by wenzelm
tuned;
2014-11-05, by wenzelm
more frugal keywords;
2014-11-05, by wenzelm
eliminated pointless dynamic keywords (TTY legacy);
2014-11-05, by wenzelm
explicit type Keyword.keywords;
2014-11-05, by wenzelm
tuned;
2014-11-05, by wenzelm
clarified representation of type Keywords;
2014-11-05, by wenzelm
explicit type Keyword.Keywords;
2014-11-05, by wenzelm
clarified minor/major lexicon (like ML version);
2014-11-05, by wenzelm
reduced execution time
2014-11-05, by nipkow
proper button margins for Nimbus L&F;
2014-11-04, by wenzelm
approximative update of versions;
2014-11-04, by wenzelm
Added Option.bind_split{,_asm,s}
2014-11-04, by lammich
clarified legacy code;
2014-11-03, by wenzelm
eliminated unused int_only flag (see also c12484a27367);
2014-11-03, by wenzelm
eliminated obsolete Proof.goal_message -- print outcome more directly;
2014-11-03, by wenzelm
updated to scala-2.11.4;
2014-11-03, by wenzelm
less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;
2014-11-02, by wenzelm
modernized header uniformly as section;
2014-11-02, by wenzelm
prefer \setisabellecontext;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
obsolete;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
obsolete;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
clarified legacy command;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
obsolete;
2014-11-02, by wenzelm
added update_header tool;
2014-11-02, by wenzelm
modernized header;
2014-11-02, by wenzelm
more flexibile \setisabellecontext, independently of header;
2014-11-02, by wenzelm
prefer explicit heading command;
2014-11-02, by wenzelm
uniform heading commands work in any context, even in theory header;
2014-11-02, by wenzelm
eliminated dead code;
2014-11-02, by wenzelm
clarified syntax -- avoid overlap with command category;
2014-11-01, by wenzelm
tuned signature (see ab2483fad861);
2014-11-01, by wenzelm
recover via scanner;
2014-11-01, by wenzelm
simplified -- scanning is never interactive;
2014-11-01, by wenzelm
tuned signature, in accordance to Scala version;
2014-11-01, by wenzelm
command-line terminator ";" is no longer accepted;
2014-11-01, by wenzelm
eliminated spurious semicolons;
2014-11-01, by wenzelm
eliminated former Proof General preferences;
2014-11-01, by wenzelm
merged
2014-10-31, by wenzelm
tuned;
2014-10-31, by wenzelm
provide explicit theory (amending 621c052789b4);
2014-10-31, by wenzelm
removed pointless markup;
2014-10-31, by wenzelm
discontinued obsolete \<^sync> marker;
2014-10-31, by wenzelm
discontinued obsolete control command category;
2014-10-31, by wenzelm
obsolete;
2014-10-31, by wenzelm
obsolete;
2014-10-31, by wenzelm
discontinued obsolete tty and prompt;
2014-10-31, by wenzelm
discontinued pointless option: timing is always on (overall theory only);
2014-10-31, by wenzelm
eliminated odd flags and hook;
2014-10-31, by wenzelm
avoid noise (cf. 03ff4d1e6784);
2014-10-31, by wenzelm
discontinued Isar TTY loop;
2014-10-31, by wenzelm
removed obsolete Proof General commands;
2014-10-31, by wenzelm
obsolete;
2014-10-31, by wenzelm
discontinued obsolete Output.urgent_message;
2014-10-31, by wenzelm
discontinued Proof General;
2014-10-31, by wenzelm
Some comments and a new version of a result
2014-10-31, by paulson
merged
2014-10-30, by wenzelm
eliminated aliases;
2014-10-30, by wenzelm
eliminated aliases;
2014-10-30, by wenzelm
eliminated aliases;
2014-10-30, by wenzelm