Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-4096
+4096
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
avoid ligatures;
2015-11-04, by wenzelm
added propertional dashes from DejaVuSans (not Mono): 0x2013, 0x2014, 0x2015;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
tuned whitespace;
2015-11-04, by wenzelm
updated;
2015-11-04, by wenzelm
more antiquotations;
2015-11-04, by wenzelm
document antiquotation @{footnote};
2015-11-04, by wenzelm
dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
2015-11-04, by wenzelm
eliminated Nitpick's pedantic support for 'emdash'
2015-11-04, by blanchet
tuned;
2015-11-04, by wenzelm
NEWS;
2015-11-04, by wenzelm
Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04, by ballarin
Qualifiers in locale expressions default to mandatory regardless of the command.
2015-11-04, by ballarin
merged
2015-11-03, by wenzelm
tuned signature;
2015-11-03, by wenzelm
prefer Isabelle/Scala Future;
2015-11-03, by wenzelm
prefer Isabelle/Scala Future;
2015-11-03, by wenzelm
tuned imports;
2015-11-03, by wenzelm
more direct task future implementation, with proper cancel operation;
2015-11-03, by wenzelm
tuned;
2015-11-03, by wenzelm
prefer ad-hoc non-worker threads;
2015-11-03, by wenzelm
clarified modules;
2015-11-03, by wenzelm
cancel already running request;
2015-11-03, by wenzelm
added acknowledgement in Binomial.thy
2015-11-03, by eberlm
Merged
2015-11-03, by eberlm
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02, by eberlm
don't pollute local theory with needless names
2015-11-02, by blanchet
allow selectors and discriminators with same name as type
2015-11-02, by blanchet
make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
2015-11-02, by blanchet
merged
2015-11-02, by wenzelm
avoid premature flushing and thus flashing of text area;
2015-11-02, by wenzelm
tuned whitespace;
2015-11-02, by wenzelm
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
2015-11-02, by wenzelm
redundant;
2015-11-02, by wenzelm
tuned whitespace;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
tuned document;
2015-11-02, by wenzelm
isabelle update_cartouches -t;
2015-11-02, by wenzelm
avoid highlighted area getting "stuck" after edit;
2015-11-02, by wenzelm
clarified completion of Isabelle symbols within document source;
2015-11-02, by wenzelm
more accurate imports: allow re-uses of base names in PIDE interaction (amending 60c159d490a2);
2015-11-02, by wenzelm
merged
2015-11-02, by nipkow
tuned names and optimized comparison order
2015-11-02, by nipkow
updated CVC4 component to deal with paths with whitespace
2015-11-02, by blanchet
Merged
2015-11-02, by eberlm
Rounding function, uniform limits, cotangent, binomial identities
2015-11-02, by eberlm
merged
2015-10-31, by wenzelm
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
2015-10-31, by wenzelm
global start time as reference point;
2015-10-31, by wenzelm
tuned signature -- clarified modules;
2015-10-30, by wenzelm
obsolete (see 9c6346319eee, 7924d61b50cf);
2015-10-30, by wenzelm
added splay trees
2015-10-30, by nipkow
added many small lemmas about setsum/setprod/powr/...
2015-10-29, by eberlm
no icons here -- not a standalone window;
2015-10-27, by wenzelm
workaround for problem with C-1, C-2, C-3 seen on Slovak QWERTY keyboard;
2015-10-27, by wenzelm
removed presumably obsolete workaround (see 7924d61b50cf);
2015-10-27, by wenzelm
Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-27, by paulson
merged
2015-10-26, by paulson
new lemmas about topology, etc., for Cauchy integral formula
2015-10-26, by paulson
adapted to 436b7fe89cdc
2015-10-26, by nipkow
clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
2015-10-26, by wenzelm
added 234-trees (slow)
2015-10-25, by nipkow
added 234-Trees (slow)
2015-10-25, by nipkow
tuned
2015-10-25, by nipkow
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
2015-10-24, by wenzelm
updated to jedit-5.3.0 and SideKick 1.8;
2015-10-23, by wenzelm
updated to jdk-8u66;
2015-10-23, by wenzelm
print thm wrt. local shyps (from full proof context);
2015-10-23, by wenzelm
clarified modules;
2015-10-23, by wenzelm
proper transfer of stored facts;
2015-10-23, by wenzelm
tuned;
2015-10-22, by wenzelm
more robust ASCII output: avoid ligatures of quotes;
2015-10-22, by wenzelm
tuned;
2015-10-22, by wenzelm
more control symbols;
2015-10-22, by wenzelm
clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;
2015-10-22, by wenzelm
rendering for \<^verbatim>;
2015-10-21, by wenzelm
Isabelle fonts via external component;
2015-10-21, by wenzelm
tuned document;
2015-10-21, by wenzelm
tuned document;
2015-10-21, by wenzelm
added glyphs 0x25a9 from DejaVuSansMono;
2015-10-21, by wenzelm
removed generated files from repository;
2015-10-21, by wenzelm
tuned;
2015-10-21, by wenzelm
proper spaces around @{text};
2015-10-21, by wenzelm
isabelle update_cartouches -t;
2015-10-20, by wenzelm
added isabelle update_cartouches option -t;
2015-10-20, by wenzelm
another antiquotation short form: undecorated cartouche as alias for @{text};
2015-10-20, by wenzelm
repaired document;
2015-10-19, by wenzelm
more symbols;
2015-10-19, by wenzelm
tuned English;
2015-10-19, by wenzelm
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
2015-10-19, by wenzelm
tuned document;
2015-10-19, by wenzelm
merged
2015-10-19, by wenzelm
avoid odd permissions of fresh tmp_file;
2015-10-19, by wenzelm
added action "isabelle-emph";
2015-10-19, by wenzelm
tuned;
2015-10-19, by wenzelm
tuned;
2015-10-19, by wenzelm
tuned text
2015-10-19, by nipkow
tuned;
2015-10-18, by wenzelm
merged
2015-10-18, by wenzelm
more control symbols;
2015-10-18, by wenzelm
tuned signature;
2015-10-18, by wenzelm
tuned signature;
2015-10-18, by wenzelm
clarified;
2015-10-18, by wenzelm
clarified control antiquotations: decode control symbol to get name;
2015-10-18, by wenzelm
more documentation;
2015-10-18, by wenzelm
support control symbol antiquotations;
2015-10-18, by wenzelm
clarified Symbol.is_control;
2015-10-18, by wenzelm
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
2015-10-18, by nipkow
code abbreviation for mapping over a fixed range
2015-10-17, by haftmann
back to lxbroy3, which appears to be free at the moment;
2015-10-17, by wenzelm
tuned signature;
2015-10-17, by wenzelm
merged
2015-10-17, by wenzelm
more uniform command setup;
2015-10-17, by wenzelm
added 'paragraph', 'subparagraph';
2015-10-17, by wenzelm
clarified Latex.environment;
2015-10-17, by wenzelm
more explicit output of list items;
2015-10-17, by wenzelm
tuned;
2015-10-17, by wenzelm
clarified nesting of paragraphs: indentation is taken into account more uniformly;
2015-10-17, by wenzelm
Markdown support in document text;
2015-10-16, by wenzelm
clarified Antiquote.antiq_reports;
2015-10-16, by wenzelm
trim_blanks after read, before eval;
2015-10-15, by wenzelm
clarified modules;
2015-10-15, by wenzelm
load markdown.ML into Pure;
2015-10-15, by wenzelm
proper recursive nesting of adjacent lists;
2015-10-15, by wenzelm
tuned;
2015-10-15, by wenzelm
clarified line content: source without marker prefix;
2015-10-15, by wenzelm
more markup;
2015-10-15, by wenzelm
report Markdown document structure;
2015-10-15, by wenzelm
more comments;
2015-10-15, by wenzelm
unused -- avoid confusion in Symbols dockable;
2015-10-15, by wenzelm
proper nesting of adjacent lists;
2015-10-15, by wenzelm
more document structure;
2015-10-15, by wenzelm
more document structure;
2015-10-14, by wenzelm
more document structure;
2015-10-14, by wenzelm
clarified;
2015-10-14, by wenzelm
minimal support for Markdown documents;
2015-10-14, by wenzelm
clarified;
2015-10-14, by wenzelm
more symbols;
2015-10-14, by wenzelm
more symbols;
2015-10-14, by wenzelm
clarified control symbols;
2015-10-14, by wenzelm
added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono;
2015-10-14, by wenzelm
tuned signature (cf. XML.trim_blanks);
2015-10-13, by wenzelm
added split_lines;
2015-10-13, by wenzelm
qualify some names stemming from internal bootstrap constructions
2015-10-17, by haftmann
removed too aggressive underscorization
2015-10-15, by blanchet
typo
2015-10-13, by nipkow
prefer undecorated typedef
2015-10-13, by nipkow
even -> evn to avoid clash with global even
2015-10-13, by nipkow
added invar empty
2015-10-13, by nipkow
Fixed nonterminating "blast" proof
2015-10-13, by paulson
new material on path_component_sets, inside, outside, etc. And more default simprules
2015-10-13, by paulson
restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
2015-10-13, by haftmann
prod_case as canonical name for product type eliminator
2015-10-13, by haftmann
emphasized general nature of parameter
2015-10-13, by haftmann
moved lemmas
2015-10-13, by haftmann
more symbols;
2015-10-12, by wenzelm
redundant due to \parindent 0pt;
2015-10-12, by wenzelm
isabelle update_cartouches;
2015-10-12, by wenzelm
scalable fonts for T1 encoding;
2015-10-12, by wenzelm
proper imports;
2015-10-12, by wenzelm
more symbols;
2015-10-12, by wenzelm
more symbols;
2015-10-12, by wenzelm
more antiquotations;
2015-10-12, by wenzelm
proper message;
2015-10-12, by wenzelm
clarified antiquotation;
2015-10-12, by wenzelm
spelling;
2015-10-12, by wenzelm
unused;
2015-10-12, by wenzelm
obsolete;
2015-10-12, by wenzelm
@{verbatim [display]} supersedes old alltt/ttbox;
2015-10-12, by wenzelm
@{verbatim [display]} supersedes old alltt/ttbox;
2015-10-12, by wenzelm
more symbols;
2015-10-12, by wenzelm
some control symbols for markup and formatting;
2015-10-12, by wenzelm
allow control symbols within markup body;
2015-10-12, by wenzelm
added glyphs 0x2501, 0x2508, 0x2509, 0x25aa, 0x25b8 from DejaVuSansMono;
2015-10-12, by wenzelm
proper document source;
2015-10-11, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- less symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
tuned whitespace;
2015-10-10, by wenzelm
tuned;
2015-10-10, by wenzelm
tuned syntax -- more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
more symbols;
2015-10-10, by wenzelm
prefer symbols;
2015-10-10, by wenzelm
use Isabelle symbols by default;
2015-10-10, by wenzelm
isabelle update_cartouches;
2015-10-10, by wenzelm
more explicit HTML.symbols;
2015-10-10, by wenzelm
NEWS;
2015-10-09, by wenzelm
more direct HTML presentation, without print mode;
2015-10-09, by wenzelm
discontinued specific HTML syntax;
2015-10-09, by wenzelm
installable TTF for MS IE 9+;
2015-10-09, by wenzelm
output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-10-09, by wenzelm
tuned output;
2015-10-09, by wenzelm
server-side fonts;
2015-10-09, by wenzelm
more accurate imitation of "cp -p -f";
2015-10-09, by wenzelm
more Present operations on Scala side;
2015-10-09, by wenzelm
clarified, according to Isabelle_System.copy_file in ML;
2015-10-09, by wenzelm
NEWS
2015-10-09, by kuncar
documentation for transfer debug methods
2015-10-09, by kuncar
add a file with examples of debugging transfer
2015-10-09, by kuncar
new methods for debugging transfer and transfer_prover
2015-10-09, by kuncar
right parenthesization
2015-10-09, by kuncar
made TPTP SZS status more compliant
2015-10-08, by blanchet
tuning
2015-10-08, by blanchet
measurable sets on product spaces are embeddings of countable products
2015-10-08, by hoelzl
generalize eqI theorems for product measures
2015-10-08, by hoelzl
isabelle update_cartouches;
2015-10-07, by wenzelm
more glyphs from DejaVuSansMono and DejaVuSansMono-Bold: 0100-017F Latin Extended-A, 0180-024F Latin Extended-B;
2015-10-07, by wenzelm
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
2015-10-07, by hoelzl
avoid 'legacy binding' warning
2015-10-07, by blanchet
removed dead code
2015-10-07, by blanchet
merged
2015-10-07, by wenzelm
back to old-fashioned GC, which appears to work better with interactive applications;
2015-10-07, by wenzelm
routine check of theory context;
2015-08-31, by wenzelm
proper context;
2015-10-06, by wenzelm
proper context;
2015-10-06, by wenzelm
clarify docs
2015-10-07, by blanchet
updated docs
2015-10-07, by blanchet
made documentation more accurate
2015-10-07, by blanchet
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
2015-10-07, by blanchet
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
2015-10-06, by blanchet
parallel tests: 6h & 12h;
2015-10-06, by wenzelm
news
2015-10-06, by blanchet
generate 'case_transfer' unconditionally
2015-10-06, by blanchet
isabelle update_cartouches;
2015-10-06, by wenzelm
isabelle update_cartouches;
2015-10-06, by wenzelm
merged
2015-10-06, by wenzelm
avoid hardwired frees;
2015-10-06, by wenzelm
added Thm.forall_intr_name;
2015-10-06, by wenzelm
added 'proposition' command;
2015-10-06, by wenzelm
fewer aliases for toplevel theorem statements;
2015-10-06, by wenzelm
just one theorem kind, which is legacy anyway;
2015-10-06, by wenzelm
pretty_const: proper local name space;
2015-10-06, by wenzelm
collect the names from goals in favor of fragile exports
2015-10-06, by traytel
compile
2015-10-06, by blanchet
tuning
2015-10-06, by blanchet
avoid legacy syntax
2015-10-06, by blanchet
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
2015-10-05, by blanchet
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
2015-10-05, by blanchet
merged
2015-10-05, by wenzelm
tuned signature;
2015-10-05, by wenzelm
produce nodes_status outside GUI thread, to avoid a few milliseconds of blocking;
2015-10-05, by wenzelm
avoid too aggressive optimization of 'finite' predicate
2015-10-05, by blanchet
avoid unsound simplification of (C (s x)) when s is a selector but not C's
2015-10-05, by blanchet
extended theory exporter to also export MePo-selected facts
2015-10-05, by blanchet
speed up MaSh duplicate check
2015-10-04, by blanchet
sped up MaSh nickname generation
2015-10-04, by blanchet
merged
2015-10-03, by wenzelm
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
2015-10-02, by wenzelm
speed up MaSh
2015-10-03, by blanchet
updated docs and NEWS
2015-10-02, by blanchet
updated docs
2015-10-02, by blanchet
removed Nitpick nonblocking mode, that was never really used
2015-10-02, by blanchet
adapted example
2015-10-02, by blanchet
removed obsolete material in documentation
2015-10-02, by blanchet
further reduced dependency on legacy async thread manager
2015-10-02, by blanchet
removed legacy asynchronous mode in Sledgehammer
2015-10-02, by blanchet
better compliance with TPTP SZS standard
2015-10-02, by blanchet
merged
2015-10-02, by wenzelm
avoid useless empty case_names;
2015-10-02, by wenzelm
clarified init (again): isabelle.Main is responsible to provide basic JVM setup, jedit.jar picks this up (e.g. list of known fonts), plugin cannot be loaded in isolation without isabelle.Main;
2015-10-02, by wenzelm
New theorems about connected sets. And pairwise moved to Set.thy.
2015-10-02, by paulson
less ambitious regex -- avoid unclarities of escaping;
2015-10-01, by wenzelm
tuned documentation
2015-10-01, by blanchet
tuned datatype docs
2015-10-01, by blanchet
export proof method in signature
2015-10-01, by blanchet
export '_cmd' functions
2015-10-01, by blanchet
back to old JavaAppLauncher to avoid initial startup problems (due to unsigned application?);
2015-09-30, by wenzelm
tuned GUI;
2015-09-30, by wenzelm
proper isabelle.root for bootstrap;
2015-09-30, by wenzelm
merged
2015-09-30, by wenzelm
tuned;
2015-09-30, by wenzelm
proper Cygwin.init (amending e00e1bf23d03);
2015-09-30, by wenzelm
renamed jvmpath to platform_path;
2015-09-30, by wenzelm
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
2015-09-30, by wenzelm
tuned GUI;
2015-09-30, by wenzelm
uniform treatment of bootstrap directories;
2015-09-30, by wenzelm
more robust system init (again), in case the plugin is started without isabelle.Main;
2015-09-30, by wenzelm
tuned message;
2015-09-30, by wenzelm
clarified modules;
2015-09-30, by wenzelm
Merge
2015-09-30, by paulson
Dead wood removal
2015-09-30, by paulson
Merge
2015-09-30, by paulson
real_of_nat_Suc is now a simprule
2015-09-30, by paulson
updated docs
2015-09-30, by blanchet
clarified Isabelle_System.init;
2015-09-29, by wenzelm
tuned;
2015-09-29, by wenzelm
tuned GUI;
2015-09-29, by wenzelm
proper event;
2015-09-29, by wenzelm
tuned GUI;
2015-09-29, by wenzelm
build session within running jEdit;
2015-09-29, by wenzelm
clarified modules;
2015-09-29, by wenzelm
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-09-27, by haftmann
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
2015-09-27, by haftmann
Caratheodory: cleanup and modernisation
2015-09-28, by hoelzl
restructure fresh variable generation to make exports more wellformed
2015-09-25, by traytel
more canonical context threading
2015-09-25, by traytel
merged
2015-09-25, by wenzelm
documentation for "Semantic subtype definitions";
2015-09-25, by wenzelm
moved remaining display.ML to more_thm.ML;
2015-09-25, by wenzelm
less redundant output;
2015-09-25, by wenzelm
proper context;
2015-09-25, by wenzelm
tuned;
2015-09-25, by wenzelm
tuned;
2015-09-25, by wenzelm
tuned;
2015-09-25, by wenzelm
tuned signature: eliminated pointless type Context.pretty;
2015-09-25, by wenzelm
more explicit Defs.context: use proper name spaces as far as possible;
2015-09-24, by wenzelm
explicit indication of overloaded typedefs;
2015-09-24, by wenzelm
tuned signature;
2015-09-23, by wenzelm
tuned output;
2015-09-23, by wenzelm
tuned output;
2015-09-23, by wenzelm
tuned signature;
2015-09-22, by wenzelm
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
2015-09-22, by wenzelm
tuned signature;
2015-09-22, by wenzelm
tuned output;
2015-09-22, by wenzelm
separate command 'print_definitions';
2015-09-22, by wenzelm
tuned;
2015-09-22, by wenzelm
clarified deps entry: global names for arguments;
2015-09-22, by wenzelm
renamed Defs.node to Defs.item;
2015-09-22, by wenzelm
tuned signature;
2015-09-22, by wenzelm
tuned whitespace;
2015-09-22, by wenzelm
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
2015-09-22, by wenzelm
prove Liminf_inverse_ereal
2015-09-25, by hoelzl
merged
2015-09-24, by immler
exchange uniform limit and integral
2015-09-24, by immler
congruence rules for the relator
2015-09-24, by traytel
conceal only the definitional theorems of map, set, rel (and not the actual constants)
2015-09-24, by traytel
more useful properties of the relators
2015-09-24, by traytel
tuned proofs (less warnings)
2015-09-24, by traytel
Useful facts about min/max, etc.
2015-09-23, by paulson
Merge
2015-09-23, by paulson
fixed a VERY SLOW proof
2015-09-23, by paulson
SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
2015-09-22, by paulson
New lemmas
2015-09-22, by paulson
Prepared two non-terminating proofs; no obvious link with my changes
2015-09-22, by paulson
added AVL and lookup function
2015-09-23, by nipkow
tuned
2015-09-23, by nipkow
merged
2015-09-22, by nipkow
unified isin-proofs
2015-09-22, by nipkow
tuned
2015-09-22, by haftmann
include some data structures into code generation
2015-09-22, by haftmann
effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
2015-09-22, by haftmann
tuned references
2015-09-22, by nipkow
added red black trees
2015-09-22, by nipkow
clarified markup;
2015-09-21, by wenzelm
isabelle update_cartouches;
2015-09-21, by wenzelm
merged
2015-09-21, by wenzelm
tuned GUI;
2015-09-21, by wenzelm
removed auto update -- bad reactivity;
2015-09-21, by wenzelm
clarified isabelle.update-state;
2015-09-21, by wenzelm
more reactive update, like Output panel;
2015-09-21, by wenzelm
added isabelle update_then;
2015-09-21, by wenzelm
NEWS;
2015-09-21, by wenzelm
tuned priority (like other query operations, e.g. "find_theorems");
2015-09-21, by wenzelm
option editor_output_state;
2015-09-21, by wenzelm
obsolete, superseded by State panel;
2015-09-21, by wenzelm
added action "isabelle-update-state";
2015-09-21, by wenzelm
support for auto update via caret focus;
2015-09-21, by wenzelm
tuned signature;
2015-09-21, by wenzelm
separate panel for proof state output;
2015-09-21, by wenzelm
tuned;
2015-09-21, by wenzelm
more specific name to reduce danger of clash with direct uses of plain Command.print_function;
2015-09-21, by wenzelm
tuned;
2015-09-21, by wenzelm
new lemmas and movement of lemmas into place
2015-09-21, by paulson
New subdirectory for functional data structures
2015-09-21, by nipkow
Added new simplifier predicate ASSUMPTION
2015-09-21, by nipkow
eliminated suspicious unicode;
2015-09-19, by wenzelm
eliminated hard tabs;
2015-09-19, by wenzelm
obsolete;
2015-09-19, by wenzelm
NEWS;
2015-09-19, by wenzelm
straight-forward refresh, without special preconditions;
2015-09-19, by wenzelm
eliminated pointless jedit_text_overview_limit;
2015-09-19, by wenzelm
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
2015-09-19, by wenzelm
allow to cancel running event;
2015-09-19, by wenzelm
tuned;
2015-09-19, by wenzelm
tuned signature;
2015-09-19, by wenzelm
Merge
2015-09-18, by paulson
Massive revisions, as a valid path must now be continously differentiable (C!)
2015-09-18, by paulson
isabelle update_cartouches;
2015-09-17, by wenzelm
isabelle update_cartouches;
2015-09-17, by wenzelm
recode all text, which is relevant for Session.save on non-ASCII directory;
2015-09-16, by wenzelm
tuned;
2015-09-16, by wenzelm
more recent JavaAppLauncher, which supports file associations;
2015-09-16, by wenzelm
more explicit indication of bundled jdk, which is required for newer versions of JavaAppLauncher;
2015-09-16, by wenzelm
more app properties glimpsed from infinitekind/Moneydance 2015.5;
2015-09-16, by wenzelm
tuned whitespace;
2015-09-16, by wenzelm
updated to polyml-5.5.3-20150916 (polyml git version cb1b36caa242);
2015-09-16, by wenzelm
avoid module dependency cycles
2015-09-15, by Andreas Lochbihler
goali -> i
2015-09-15, by nipkow
Omega_Words_Fun: Infinite words as functions from nat.
2015-09-15, by lammich
provide FontMapper for embedded fonts;
2015-09-14, by wenzelm
avoid hardwired colors;
2015-09-14, by wenzelm
avoid hardwired colors;
2015-09-14, by wenzelm
replacement character for spaces;
2015-09-14, by wenzelm
single-instance application, even on Linux;
2015-09-14, by wenzelm
single-instance application for Linux;
2015-09-14, by wenzelm
tuned message;
2015-09-14, by wenzelm
added isabelle jedit_client;
2015-09-14, by wenzelm
tuned proofs -- less legacy;
2015-09-13, by wenzelm
tuned message;
2015-09-13, by wenzelm
tuned proofs;
2015-09-13, by wenzelm
renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-13, by wenzelm
tuned proofs;
2015-09-13, by wenzelm
method "goals" ignores facts;
2015-09-13, by wenzelm
tuned;
2015-09-13, by wenzelm
unconceal symbols stemming from inductive_set specifications, which are regular part of user-space specification;
2015-09-10, by haftmann
fully detached test run, to avoid flashing window on Windows with Cygwin-Terminal;
2015-09-11, by wenzelm
single-instance application on Windows;
2015-09-11, by wenzelm
more robust init_components: test run of polyml executable on windows appears to disrupt stdin stream of cygwin;
2015-09-11, by wenzelm
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
2015-09-11, by wenzelm
clarified order;
2015-09-11, by wenzelm
more symbols;
2015-09-11, by wenzelm
Unicode is standard in Poly/ML repository version;
2015-09-10, by wenzelm
removed obsolete undocumented feature;
2015-09-10, by wenzelm
more standard local_theory operations;
2015-09-10, by wenzelm
HOL-Proofs is slow;
2015-09-10, by wenzelm
convenient access to application properties;
2015-09-10, by wenzelm
tuned -- avoid slightly odd @{cpat};
2015-09-10, by wenzelm
dropped redundant NEWS
2015-09-10, by haftmann
less ambitious options, to accomodate 4GB systems;
2015-09-10, by wenzelm
tuned
2015-09-10, by nipkow
clarified declaration flags, like 'declaration' command;
2015-09-09, by wenzelm
merged
2015-09-09, by wenzelm
simplified simproc programming interfaces;
2015-09-09, by wenzelm
eliminated \<Colon> from syntax of constraints;
2015-09-09, by wenzelm
eliminated \<Colon> -- from dead code!
2015-09-09, by wenzelm
merged
2015-09-09, by Andreas Lochbihler
reactivate examples with predicate compiler and quickcheck
2015-09-09, by Andreas Lochbihler
disable jedit_auto_resolve (again) -- too confusing;
2015-09-08, by wenzelm
proper Windows path, notably for ML basis;
2015-09-08, by wenzelm
more basic Windows path operations -- evade exception InvalidArc with Unicode;
2015-09-08, by wenzelm
updated to polyml-5.5.3-20150908, with support for x86_64-windows and Unicode file-names;
2015-09-08, by wenzelm
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
2015-09-08, by wenzelm
clarified Java runtime options for 32 vs. 64 bit;
2015-09-08, by wenzelm
clarified JEDIT_JAVA_OPTIONS: separate defaults for 32 vs. 64 bit;
2015-09-08, by wenzelm
clarified JEDIT_JAVA_SYSTEM_OPTIONS;
2015-09-08, by wenzelm
clarified ISABELLE_BUILD_JAVA_OPTIONS;
2015-09-08, by wenzelm
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup
2015-09-06, by haftmann
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
2015-09-06, by haftmann
formally regenerated
2015-09-06, by haftmann
tuned notation, proofs, namespace
2015-09-06, by haftmann
obsolete: if case_prod is fully applied, it is printed as proper case expression;
2015-09-06, by haftmann
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-09-06, by haftmann
tuned
2015-09-06, by haftmann
obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
2015-09-06, by haftmann
dropped whitespace leftover from b57df8eecad6
2015-09-06, by haftmann
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-09-06, by wenzelm
tuned proofs;
2015-09-06, by wenzelm
removed obsolete theory Legacy_Mrec;
2015-09-06, by wenzelm
NEWS;
2015-09-06, by wenzelm
merged
2015-09-04, by wenzelm
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
2015-09-04, by wenzelm
modernized name space management -- more uniform qualification;
2015-09-04, by wenzelm
tuned -- do not open ML structures;
2015-09-04, by wenzelm
trim context for persistent storage;
2015-09-04, by wenzelm
trim context for persistent storage;
2015-09-04, by wenzelm
proper restore naming after close, which is important for packages that used nested targets internally, e.g. BNF datatype;
2015-09-04, by wenzelm
more general Typedef.bindings;
2015-09-03, by wenzelm
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
2015-09-03, by wenzelm
merged
2015-09-04, by Andreas Lochbihler
merged
2015-09-03, by Andreas Lochbihler
use quotient and lifting package;
2015-09-03, by Andreas Lochbihler
merged
2015-09-03, by paulson
new lemmas about vector_derivative, complex numbers, paths, etc.
2015-09-03, by paulson
trim context for persistent storage;
2015-09-03, by wenzelm
misc tuning and modernization;
2015-09-03, by wenzelm
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
2015-09-03, by traytel
clean name as in ML Completion.make;
2015-09-03, by wenzelm
use alphabetic order before history order;
2015-09-03, by wenzelm
eliminated pointless cterms;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
more thorough transfer;
2015-09-02, by wenzelm
clarified context;
2015-09-02, by wenzelm
more thorough transfer;
2015-09-02, by wenzelm
clarified context;
2015-09-02, by wenzelm
tuned message;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
trim context for persistent storage;
2015-09-02, by wenzelm
eliminated old 'defs';
2015-09-02, by wenzelm
expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;
2015-09-02, by wenzelm
clarified vacuous binding;
2015-09-02, by wenzelm
trim context more thoroughly;
2015-09-02, by wenzelm
tuned;
2015-09-02, by wenzelm
updated sessions;
2015-09-02, by wenzelm
thread context for exceptions from forks, e.g. relevant when printing errors;
2015-09-01, by wenzelm
eliminated \<Colon>;
2015-09-01, by wenzelm
tuned -- avoid slightly odd @{cpat};
2015-09-01, by wenzelm
support x86_64-windows;
2015-08-31, by wenzelm
misc tuning and simplification;
2015-08-31, by wenzelm
proper option, not catch-all pattern;
2015-08-31, by wenzelm
support x86_64-windows;
2015-08-31, by wenzelm
prefer symbols;
2015-08-31, by wenzelm
prefer symbols;
2015-08-31, by wenzelm
proper qualified naming;
2015-08-31, by wenzelm
misc tuning and clarification;
2015-08-31, by wenzelm
misc tuning and modernization;
2015-08-31, by wenzelm
clarified context;
2015-08-31, by wenzelm
tuned signature;
2015-08-31, by wenzelm
clarified context;
2015-08-31, by wenzelm
tuned message;
2015-08-31, by wenzelm
trim context for persistent storage;
2015-08-31, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
store result of swapify, to avoid later access to implicit context;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
tuned;
2015-08-30, by wenzelm
clarified implicit context;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
trim context for persistent storage;
2015-08-30, by wenzelm
clarified exceptions;
2015-08-30, by wenzelm
tuned documentation -- merge is implicitly performed by the system;
2015-08-28, by wenzelm
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
2015-08-28, by wenzelm
more abstract theory certificate, which is not necessarily the full theory;
2015-08-28, by wenzelm
eliminated obsolete environment variable
2015-08-28, by blanchet
tuned signature;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned signature;
2015-08-28, by wenzelm
tuned;
2015-08-28, by wenzelm
tuned signature;
2015-08-28, by wenzelm
clarified language context, e.g. relevant for symbols;
2015-08-28, by wenzelm
merged;
2015-08-28, by wenzelm
tuned;
2015-08-26, by wenzelm
generate proper error instead of exception if goal cannot be atomized
2015-08-27, by blanchet
standardized some occurences of ancient "split" alias
2015-08-27, by haftmann
more lemmas on sorting and multisets (due to Thomas Sewell)
2015-08-27, by haftmann
robust handling of Vampire 4 proofs
2015-08-27, by blanchet
reverted 6ac3172985d4 -- the old URL has been restored
2015-08-27, by blanchet
fixed typo in comment
2015-08-27, by blanchet
use fancy options of Java 8;
2015-08-26, by wenzelm
tuned signature;
2015-08-26, by wenzelm
clarified kill on Windows: just one executable;
2015-08-26, by wenzelm
avoid deprecated PluginOptions with its unbounded window size;
2015-08-25, by wenzelm
clarified undefined_blobs: already loaded theories are suppressed;
2015-08-25, by wenzelm
tuned spacing
2015-08-25, by nipkow
tuned exercise
2015-08-25, by nipkow
merged
2015-08-24, by wenzelm
reset focus after thread update (with new debug_states);
2015-08-24, by wenzelm
atomic Debugger.status;
2015-08-24, by wenzelm
tuned;
2015-08-24, by wenzelm
tuned;
2015-08-24, by wenzelm
more thorough GUI update;
2015-08-24, by wenzelm
maintain per-thread focus context;
2015-08-24, by wenzelm
typos
2015-08-24, by nipkow
nex exercise
2015-08-24, by nipkow
more explicit debugger caret rendering;
2015-08-24, by wenzelm
more explicit type Debugger.Context;
2015-08-23, by wenzelm
more precise tree re-selection;
2015-08-23, by wenzelm
proper GUI event;
2015-08-23, by wenzelm
update focus more thoroughly;
2015-08-23, by wenzelm
tuned;
2015-08-22, by wenzelm
merged
2015-08-21, by traytel
don't use types that come from the database---they are inconsistent with the ones occurring in the terms
2015-08-21, by traytel
tuned;
2015-08-21, by wenzelm
clarified linux application bundle;
2015-08-21, by wenzelm
more version information;
2015-08-21, by wenzelm
separate bundle for windows64;
2015-08-21, by wenzelm
tuned;
2015-08-21, by wenzelm
more scalable GUI;
2015-08-21, by wenzelm
eliminated WinRun4J artifact;
2015-08-21, by wenzelm
proper classpath for launcher;
2015-08-21, by wenzelm
updated to jdk-8u60, with support for x86_64-windows;
2015-08-21, by wenzelm
updated to recent launch4j 3.8;
2015-08-21, by wenzelm
clarified modules;
2015-08-20, by wenzelm
clarified modules, like ML version;
2015-08-20, by wenzelm
clarified modules, like ML version;
2015-08-20, by wenzelm
suppress small CPU time, notably on x86-windows, where bash does not account for the poly process;
2015-08-20, by wenzelm
obsolete;
2015-08-20, by wenzelm
tuned signature, according to ML version;
2015-08-20, by wenzelm
The Stone-Weierstrass theorem
2015-08-20, by paulson
tuned;
2015-08-20, by wenzelm
obsolete;
2015-08-20, by wenzelm
NEWS;
2015-08-20, by wenzelm
updated to polyml-5.5.3-20150820, with native x86-windows support;
2015-08-20, by wenzelm
precise BinIO, without newline conversion on Windows;
2015-08-20, by wenzelm
repaired proofs after 6a6f15d8fbc4;
2015-08-19, by wenzelm
merged
2015-08-19, by wenzelm
clarified x86-windows setup;
2015-08-19, by wenzelm
proper check for Windows executables;
2015-08-19, by wenzelm
Cygwin bash on Windows;
2015-08-19, by wenzelm
tuned;
2015-08-19, by wenzelm
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
2015-08-19, by wenzelm
New material and fixes related to the forthcoming Stone-Weierstrass development
2015-08-19, by paulson
disabled auto resolve, until practical consequences are more clear;
2015-08-19, by wenzelm
example options;
2015-08-18, by wenzelm
proper platform_path;
2015-08-18, by wenzelm
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
2015-08-18, by wenzelm
SOMEthing went wrong in eb87fc42825c;
2015-08-18, by wenzelm
include libgmp;
2015-08-18, by wenzelm
proper platform path for intial PolyML.SaveState.loadState;
2015-08-18, by wenzelm
proper platform path for initial load;
2015-08-18, by wenzelm
tuned signature;
2015-08-18, by wenzelm
keep native CInterface to make SHA1 work properly;
2015-08-18, by wenzelm
more setup for native Windows (Pure and HOL session with image);
2015-08-18, by wenzelm
basic setup for native Windows (RAW session without image);
2015-08-17, by wenzelm
more complete build;
2015-08-17, by wenzelm
support for native x86-windows via MinGW32;
2015-08-17, by wenzelm
no ML_debugger support in Pure -- too complicated;
2015-08-17, by wenzelm
more careful propagation of ML_debugger option to Pure;
2015-08-17, by wenzelm
support for ML files with/without debugger information;
2015-08-17, by wenzelm
explicit debug flag for ML compiler;
2015-08-17, by wenzelm
tuned;
2015-08-17, by wenzelm
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);
2015-08-17, by wenzelm
clarified initial ML name space (amending 7aad4be8a48e);
2015-08-16, by wenzelm
produce certified vars without access to theory_of_thm, and without context;
2015-08-16, by wenzelm
produce certified vars without access to theory_of_thm, and without context;
2015-08-16, by wenzelm
tuned;
2015-08-16, by wenzelm
added Thm.chyps_of;
2015-08-16, by wenzelm
prefer theory_id operations;
2015-08-16, by wenzelm
separate type theory_id;
2015-08-16, by wenzelm
delete precisely the added rules;
2015-08-16, by wenzelm
clarified context;
2015-08-16, by wenzelm
tuned whitespace;
2015-08-16, by wenzelm
tuned signature;
2015-08-16, by wenzelm
tuned;
2015-08-16, by wenzelm
tuned whitespace;
2015-08-15, by wenzelm
tuned whitespace;
2015-08-15, by wenzelm
obsolete;
2015-08-15, by wenzelm
clarified context;
2015-08-15, by wenzelm
clarified context;
2015-08-15, by wenzelm
tuned GUI;
2015-08-15, by wenzelm
proper setup of evaluation context;
2015-08-15, by wenzelm
tuned;
2015-08-15, by wenzelm
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
2015-08-15, by wenzelm
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);
2015-08-15, by wenzelm
tuned signature;
2015-08-15, by wenzelm
qualified adjust_*
2015-08-13, by haftmann
more lemmas
2015-08-13, by haftmann
unfold intermediate definitions (stemming from composition) in lifted bnf operations
2015-08-13, by traytel
merged
2015-08-13, by wenzelm
more standard options;
2015-08-13, by wenzelm
prefer official @{make_string};
2015-08-13, by wenzelm
tuned signature, in accordance to sortBy in Scala;
2015-08-13, by wenzelm
clarified modules;
2015-08-12, by wenzelm
tuned NEWS
2015-08-13, by traytel
actually process lift_bnf regression suite
2015-08-12, by traytel
NEWS, CONTRIBUTORS, documentation for lift_bnf
2015-08-12, by traytel
use lift_bnf in an example
2015-08-12, by traytel
new command for lifting BNF structure over typedefs
2015-08-12, by traytel
more thorough reload;
2015-08-12, by wenzelm
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
2015-08-12, by wenzelm
merged
2015-08-12, by wenzelm
tuned colors;
2015-08-12, by wenzelm
clarified breakpoint rendering;
2015-08-12, by wenzelm
clarified;
2015-08-12, by wenzelm
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
2015-08-12, by wenzelm
clarified init/exit vs. session phase;
2015-08-12, by wenzelm
clarify type vs. term instantiation when forming closure;
2015-08-12, by Daniel Matichuk
more accurate dependencies;
2015-08-11, by wenzelm
tuned;
2015-08-11, by wenzelm
clarified thread re-selection;
2015-08-11, by wenzelm
clarified tree row handling;
2015-08-11, by wenzelm
proper context (amending 7aad4be8a48e);
2015-08-11, by wenzelm
suppress threads without debug state;
2015-08-11, by wenzelm
clarified events;
2015-08-11, by wenzelm
clarified GUI event handling;
2015-08-11, by wenzelm
tuned signature;
2015-08-11, by wenzelm
tuned;
2015-08-11, by wenzelm
misc tuning and clarification;
2015-08-11, by wenzelm
print values for stack entry;
2015-08-11, by wenzelm
clarified output;
2015-08-11, by wenzelm
default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
2015-08-11, by wenzelm
clarified break *point* position;
2015-08-11, by wenzelm
support hyperlinks with optional focus change;
2015-08-11, by wenzelm
tuned;
2015-08-11, by wenzelm
vacuous input means continue, e.g. after exit;
2015-08-11, by wenzelm
GUI actions depend on active debugger;
2015-08-11, by wenzelm
init/exit depending on active debugger panels;
2015-08-11, by wenzelm
eliminated cancel operation: disrupts normal evaluation of thread;
2015-08-11, by wenzelm
register thread such that cancel works;
2015-08-11, by wenzelm
clarified default selection;
2015-08-10, by wenzelm
report final debugger_state more robustly, e.g. after interrupt;
2015-08-10, by wenzelm
eliminated global option: breakpoints control this individually;
2015-08-10, by wenzelm
more uniform ScrollPane, like graphview;
2015-08-10, by wenzelm
tuned signature;
2015-08-10, by wenzelm
tuned rendering;
2015-08-10, by wenzelm
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
2015-08-10, by wenzelm
more thorough Encode.string;
2015-08-10, by wenzelm
added action to toggle breakpoints (on editor side);
2015-08-10, by wenzelm
sort lines;
2015-08-10, by wenzelm
rendering for debugger/breakpoint active state;
2015-08-10, by wenzelm
follow debugger focus;
2015-08-10, by wenzelm
tuned signature;
2015-08-10, by wenzelm
tuned imports;
2015-08-10, by wenzelm
tuned messages;
2015-08-10, by wenzelm
clarified ML options;
2015-08-10, by wenzelm
merged
2015-08-08, by wenzelm
more single stepping;
2015-08-08, by wenzelm
direct bootstrap of integer division from natural division
2015-08-08, by haftmann
slight cleanup of lemmas
2015-08-06, by haftmann
obsolete since no code generator without dictionary construction left
2015-08-06, by haftmann
make SML/NJ work;
2015-08-07, by wenzelm
suppress empty messages as usual;
2015-08-07, by wenzelm
proper Symbol.decode/encode;
2015-08-07, by wenzelm
eval ML context;
2015-08-07, by wenzelm
maintain history more often;
2015-08-07, by wenzelm
approximate old selection after update;
2015-08-06, by wenzelm
expand all rows for robustness and simplicity;
2015-08-06, by wenzelm
evaluate ML expressions within debugger context;
2015-08-06, by wenzelm
clarified debugger loop;
2015-08-06, by wenzelm
clarified thread state;
2015-08-06, by wenzelm
tuned;
2015-08-06, by wenzelm
more controls;
2015-08-06, by wenzelm
tuned;
2015-08-06, by wenzelm
clarified signature, to make debugger.ML compile with current official ML versions;
2015-08-06, by wenzelm
support for tree selection;
2015-08-05, by wenzelm
proper dynamic update;
2015-08-05, by wenzelm
tuned;
2015-08-05, by wenzelm
more GUI components;
2015-08-05, by wenzelm
tuned;
2015-08-05, by wenzelm
tuned;
2015-08-05, by wenzelm
more controls;
2015-08-05, by wenzelm
proper initialization;
2015-08-05, by wenzelm
tuned signature;
2015-08-05, by wenzelm
protocol support for thread debugger state;
2015-08-05, by wenzelm
eliminated clone;
2015-08-04, by wenzelm
merged
2015-08-04, by wenzelm
more symbols;
2015-08-04, by wenzelm
more symbols;
2015-08-04, by wenzelm
more documentation of coercions
2015-08-04, by traytel
merged
2015-07-30, by wenzelm
clarified management of (single) session;
2015-07-30, by wenzelm
maintain debugger output messages;
2015-07-30, by wenzelm
provide CharSequence operations as well;
2015-07-30, by wenzelm
more GUI components;
2015-07-29, by wenzelm
tuned;
2015-07-29, by wenzelm
separate channel for debugger output;
2015-07-29, by wenzelm
clarified thread name;
2015-07-29, by wenzelm
add coinduction rule for infinite
2015-07-30, by Andreas Lochbihler
merged
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
more explicit context;
2015-07-28, by wenzelm
eliminated dead code;
2015-07-28, by wenzelm
clarified Variable.gen_all;
2015-07-28, by wenzelm
more explicit context;
2015-07-28, by wenzelm
more direct access to atomic cterms;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
proper context;
2015-07-28, by wenzelm
more direct access to atomic cterms;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
clarified context;
2015-07-28, by wenzelm
merged
2015-07-28, by immler
merged
2015-07-28, by immler
added theory Uniform_Limit
2015-07-28, by immler
evade timeout problem on macbroy6 (potentially due to NFS oddities);
2015-07-28, by wenzelm
tweaks. Got rid of a really slow step
2015-07-28, by paulson
the Cauchy integral theorem and related material
2015-07-28, by paulson
depth -> height; removed del_rightmost (too specifi)
2015-07-28, by nipkow
tuned;
2015-07-27, by wenzelm
merged
2015-07-27, by wenzelm
tuned signature;
2015-07-27, by wenzelm
formal class for factorial (semi)rings
2015-07-27, by haftmann
merged
2015-07-27, by wenzelm
NEWS;
2015-07-27, by wenzelm
tuned signature;
2015-07-27, by wenzelm
New material for Cauchy's integral theorem
2015-07-27, by paulson
tuned signature for print_nested_cases;
2015-07-27, by wenzelm
more explicit checks -- improved errors;
2015-07-27, by wenzelm
eliminated cterm_instantiate;
2015-07-27, by wenzelm
updated to infer_instantiate;
2015-07-27, by wenzelm
tuned signature;
2015-07-27, by wenzelm
added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;
2015-07-27, by wenzelm
eliminated atac, rtac, etac, dtac, ftac;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
proper context;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
ignore non-existant variables, like other instantiate rules;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-26, by wenzelm
added infer_instantiate';
2015-07-26, by wenzelm
more uniform exceptions, like cterm_instantiate;
2015-07-26, by wenzelm
updated to infer_instantiate;
2015-07-25, by wenzelm
more accurate maxidx;
2015-07-25, by wenzelm
clarified error;
2015-07-25, by wenzelm
added infer_instantiate, which is meant to supersede cterm_instantiate;
2015-07-25, by wenzelm
eliminated alias;
2015-07-24, by wenzelm
proper context;
2015-07-24, by wenzelm
unused;
2015-07-24, by wenzelm
proper context;
2015-07-24, by wenzelm
more symbols by default, without xsymbols mode;
2015-07-23, by wenzelm
Measures form a CCPO
2015-07-23, by hoelzl
reorganized Extended_Real
2015-07-23, by hoelzl
isabelle update_cartouches;
2015-07-23, by wenzelm
tuned proofs;
2015-07-23, by wenzelm
proper latex;
2015-07-23, by wenzelm
tuned proofs;
2015-07-22, by wenzelm
tuned proofs;
2015-07-22, by wenzelm
support for ML debugger;
2015-07-21, by wenzelm
more explicit thread identification;
2015-07-21, by wenzelm
avoid lxbroy2, lxbroy3, lxbroy4, which are often busy with other processes;
2015-07-21, by wenzelm
new material for multivariate analysis, etc.
2015-07-20, by paulson
proper LaTeX;
2015-07-20, by wenzelm
updated to jdk-8u51;
2015-07-19, by wenzelm
more symbols;
2015-07-19, by wenzelm
isabelle update_cartouches;
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
merged
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
tuned whitespace;
2015-07-18, by wenzelm
prefer tactics with explicit context;
2015-07-18, by wenzelm
reactivated dead code;
2015-07-18, by wenzelm
more uniform ComponentAdapter;
2015-07-17, by wenzelm
skeleton for interactive debugger;
2015-07-17, by wenzelm
tuned;
2015-07-17, by wenzelm
tuned;
2015-07-17, by wenzelm
store breakpoints within ML environment;
2015-07-17, by wenzelm
clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
2015-07-17, by wenzelm
report possible breakpoint positions;
2015-07-17, by wenzelm
proper attribute;
2015-07-17, by wenzelm
forgotten selector
2015-07-17, by traytel
made code less loopy
2015-07-16, by blanchet
keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)
2015-07-16, by blanchet
generalized generic translation function
2015-07-16, by blanchet
merge
2015-07-16, by blanchet
tuning
2015-07-16, by blanchet
generalized limitation in documentation
2015-07-16, by blanchet
made tactic more robust w.r.t. equations containing 'case_prod'
2015-07-16, by blanchet
merged
2015-07-16, by wenzelm
merged
2015-07-16, by wenzelm
clarified boundary cases of completion;
2015-07-16, by wenzelm
additional ML parse tree components for Poly/ML 5.5.3, or later;
2015-07-16, by wenzelm
added option ML_debugger;
2015-07-16, by wenzelm
ML debugger interface;
2015-07-16, by wenzelm
{r,e,d,f}tac with proper context in BNF
2015-07-16, by traytel
move disjoint sets to their own theory
2015-07-16, by hoelzl
back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);
2015-07-15, by wenzelm
merged
2015-07-14, by wenzelm
more explicit command-line option for isabelle build;
2015-07-14, by wenzelm
more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
2015-07-14, by wenzelm
normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
2015-07-14, by wenzelm
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
2015-07-14, by hoelzl
add continuous_onI_mono
2015-07-14, by hoelzl
tuned description
2015-07-13, by blanchet
tuning
2015-07-13, by blanchet
updated Isabelle description to CASC
2015-07-13, by blanchet
imported patch up_casc
2015-07-13, by blanchet
add emeasure_add_AE
2015-07-13, by hoelzl
stronger induction assumption in lfp_transfer and emeasure_lfp
2015-07-13, by hoelzl
refrain from testing HOL-Proofs for x86_64-linux: takes more than 4h;
2015-07-13, by wenzelm
Quickcheck setup for finite sets
2015-07-12, by Lars Hupel
tuned proofs;
2015-07-11, by wenzelm
tuned proofs;
2015-07-11, by wenzelm
merged
2015-07-09, by wenzelm
tuned proofs;
2015-07-09, by wenzelm
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
2015-07-09, by wenzelm
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
2015-07-09, by wenzelm
tuned whitespace;
2015-07-09, by wenzelm
tuned ML signature (and rationalized code a bit)
2015-07-09, by blanchet
merged
2015-07-09, by noschinl
case_of_simps: do not split for types with a single constructor
2015-07-09, by noschinl
tests for Simps_Case_Conv
2015-07-09, by noschinl
merged
2015-07-09, by wenzelm
clarified context;
2015-07-09, by wenzelm
tuned proofs;
2015-07-09, by wenzelm
clarified context;
2015-07-09, by wenzelm
clarified context;
2015-07-08, by wenzelm
Variable.focus etc.: optional bindings provided by user;
2015-07-08, by wenzelm
clarified text folds: proof ... qed counts as extra block;
2015-07-08, by wenzelm
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-07-08, by wenzelm
tuned;
2015-07-08, by wenzelm
tuned according to a81dc82ecba3;
2015-07-08, by wenzelm
tuned facts
2015-07-08, by haftmann
more cautious use of [iff] declarations
2015-07-08, by haftmann
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-07-08, by haftmann
eliminated some duplication
2015-07-08, by haftmann
more algebraic properties for gcd/lcm
2015-07-08, by haftmann
moved normalization and unit_factor into Main HOL corpus
2015-07-08, by haftmann
more generous timeout for the sake of HOL-Proofs in at64-poly;
2015-07-08, by wenzelm
tuned ML signature
2015-07-07, by blanchet
have the installed termination prover take a 'quiet' flag
2015-07-07, by blanchet
add monotonicity rule for rtranclp
2015-07-07, by hoelzl
tuned proofs;
2015-07-07, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
tuned whitespace;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned proofs;
2015-07-06, by wenzelm
plain string output, without funny control chars;
2015-07-06, by wenzelm
tuned message;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
proper outer syntax category, e.g. relevant for PIDE markup;
2015-07-06, by wenzelm
merged
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
clarified section references;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
clarified sections;
2015-07-06, by wenzelm
removed outdated and mostly obsolete material;
2015-07-06, by wenzelm
tuned;
2015-07-06, by wenzelm
tuned whitespace;
2015-07-06, by wenzelm
clarified context;
2015-07-05, by wenzelm
obsolete;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
eliminated spurious warning/tracing messages -- avoid Display.string_of_thm_without_context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
clarified context;
2015-07-05, by wenzelm
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-07-05, by wenzelm
clarified context;
2015-07-03, by wenzelm
tuned signature;
2015-07-03, by wenzelm
clarified context;
2015-07-03, by wenzelm
tuned signature;
2015-07-03, by wenzelm
generalized sup_continuty of add, ereal_of_enat
2015-07-03, by hoelzl
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-07-03, by hoelzl
moved to lxbroy3, hoping that it works better;
2015-07-02, by wenzelm
separate (semi)ring with normalization
2015-07-02, by haftmann
merged
2015-07-02, by wenzelm
more CONTRIBUTORS;
2015-07-02, by wenzelm
documentation for 'subgoal' command;
2015-07-02, by wenzelm
clarified module;
2015-07-02, by wenzelm
allow to specify suffix of goal parameters;
2015-07-02, by wenzelm
subgoal parameters are internal by default and named by user;
2015-07-02, by wenzelm
split multi-goals as usual (outermost Pure.conjunction only);
2015-07-01, by wenzelm
clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;
2015-07-01, by wenzelm
proper state after qed;
2015-07-01, by wenzelm
clarified keyword categories;
2015-07-01, by wenzelm
support for subgoal focus command;
2015-07-01, by wenzelm
tuned;
2015-07-01, by wenzelm
taylor series with has_integral and integrable_on
2015-07-01, by immler
merged
2015-06-30, by wenzelm
no arguments for "standard" (or old "default") methods;
2015-06-30, by wenzelm
renamed "default" to "standard", to make semantically clear what it is;
2015-06-30, by wenzelm
tuned;
2015-06-30, by wenzelm
Merge
2015-06-30, by paulson
Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-06-30, by paulson
generalized inf and sup_continuous; added intro rules
2015-06-30, by hoelzl
fix tex-output for rel_mset
2015-06-30, by hoelzl
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
2015-06-29, by blanchet
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
2015-06-29, by wenzelm
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-06-29, by wenzelm
clarified static phase;
2015-06-29, by wenzelm
tuned proofs;
2015-06-29, by wenzelm
more symbols;
2015-06-29, by wenzelm
more symbols;
2015-06-29, by wenzelm
corrected typo
2015-06-29, by nipkow
tuned src/HOL/ex/Ballot
2015-06-16, by hoelzl
add examples from Freek's top 100 theorems (thms 30, 73, 77)
2015-06-12, by bulwahn
generalized geometric distribution
2015-06-17, by hoelzl
added lemma
2015-06-28, by nipkow
simplified termination criterion for euclidean algorithm (again)
2015-06-27, by haftmann
tuned proof
2015-06-27, by haftmann
rings follow immediately their corresponding semirings
2015-06-27, by haftmann
tuned code setup
2015-06-27, by haftmann
algebraic specification for set gcd
2015-06-27, by haftmann
premises in 'show' are treated like 'assume';
2015-06-27, by wenzelm
adapted to a9b71c82647b;
2015-06-26, by wenzelm
merged
2015-06-26, by wenzelm
isabelle update_cartouches;
2015-06-26, by wenzelm
more symbols;
2015-06-26, by wenzelm
tuned proofs;
2015-06-26, by wenzelm
do not expose goal parameters;
2015-06-26, by wenzelm
more symbols;
2015-06-26, by wenzelm
more symbols;
2015-06-26, by wenzelm
proper spacing, as for other syntax for these symbols;
2015-06-26, by wenzelm
tuned whitespace;
2015-06-26, by wenzelm
updated SystemOnTPTP URL
2015-06-26, by blanchet
tuned proofs;
2015-06-26, by wenzelm
merged
2015-06-25, by wenzelm
implicit goal cases are legacy;
2015-06-25, by wenzelm
tuned proofs;
2015-06-25, by wenzelm
more heap -- hoping for more stability of HOL-Proofs;
2015-06-25, by wenzelm
added method "goals" for proper subgoal cases;
2015-06-25, by wenzelm
tuned signature;
2015-06-25, by wenzelm
tuned signature;
2015-06-25, by wenzelm
tuned;
2015-06-25, by wenzelm
tuned;
2015-06-25, by wenzelm
tuned signature;
2015-06-25, by wenzelm
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
2015-06-25, by haftmann
euclidean algorithm on polynomials
2015-06-25, by haftmann
more theorems
2015-06-25, by haftmann
generalized to definition from literature, which covers also polynomials
2015-06-25, by haftmann
put E before (typically remote, hence less reliable) Vampire
2015-06-25, by blanchet
tuned proofs -- less digits;
2015-06-24, by wenzelm
updated to scala-2.11.7;
2015-06-24, by wenzelm
clarified 'case' command;
2015-06-24, by wenzelm
silence 'try'
2015-06-24, by blanchet
Merge
2015-06-23, by paulson
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-23, by paulson
tuned proofs;
2015-06-23, by wenzelm
tuned proofs;
2015-06-22, by wenzelm
merged
2015-06-22, by wenzelm
tuned proofs;
2015-06-22, by wenzelm
tuned proofs;
2015-06-22, by wenzelm
tuned;
2015-06-22, by wenzelm
support 'when' statement, which corresponds to 'presume';
2015-06-22, by wenzelm
added method "sleep";
2015-06-22, by wenzelm
tuned signature;
2015-06-22, by wenzelm
tuned whitespace;
2015-06-22, by wenzelm
clarified nesting of Isar goal structure;
2015-06-22, by wenzelm
tuned;
2015-06-22, by wenzelm
keep 'Pure.all' in goals when preplaying
2015-06-22, by blanchet
use right context for preplay, to avoid errors in fact lookup
2015-06-22, by blanchet
reverted some too aggressive TPTP interpreter changes
2015-06-22, by blanchet
automatically build image
2015-06-22, by blanchet
filter out more Poly/ML messages from (ad hoc) TPTP toools
2015-06-22, by blanchet
removed (now illegal) semicolons in generated theory files
2015-06-22, by blanchet
use CVC4 instead of CVC3 at CASC
2015-06-22, by blanchet
fixed typo
2015-06-22, by blanchet
modernized name
2015-06-22, by nipkow
more symbols;
2015-06-20, by wenzelm
tuned proofs;
2015-06-20, by wenzelm
tuned proofs;
2015-06-20, by wenzelm
eliminated list_all;
2015-06-20, by wenzelm
tuned proofs;
2015-06-20, by wenzelm
tuned proofs;
2015-06-20, by wenzelm
tuned proofs;
2015-06-20, by wenzelm
isabelle update_cartouches;
2015-06-20, by wenzelm
misc tuning;
2015-06-20, by wenzelm
less ambitious USER_HOME on Windows: avoid potentially disconnected share, agree with guess of JVM user.home;
2015-06-20, by wenzelm
isabelle update_cartouches;
2015-06-20, by wenzelm
avoid suspicious Unicode;
2015-06-20, by wenzelm
tuned;
2015-06-19, by wenzelm
tuned proofs;
2015-06-19, by wenzelm
isabelle update_cartouches;
2015-06-19, by wenzelm
merged
2015-06-19, by wenzelm
removed dead code;
2015-06-19, by wenzelm
discontinued unused 'defer_recdef';
2015-06-19, by wenzelm
tuned;
2015-06-19, by wenzelm
removed dead code;
2015-06-19, by wenzelm
moved sources;
2015-06-19, by wenzelm
tuned proofs;
2015-06-19, by wenzelm
uniform system_mode for build test: avoid spurious output_dir/log that is not required later;
2015-06-19, by wenzelm
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
2015-06-19, by haftmann
generalized some theorems about integral domains and moved to HOL theories
2015-06-19, by haftmann
renamed multiset_of -> mset
2015-06-19, by nipkow
NEWS
2015-06-18, by nipkow
multiset_of_set -> mset_set
2015-06-18, by nipkow
tuned proofs -- slightly faster;
2015-06-17, by wenzelm
merged
2015-06-17, by wenzelm
tuned proofs -- slightly faster;
2015-06-17, by wenzelm
tuned proofs -- much faster;
2015-06-17, by wenzelm
tuned proofs;
2015-06-17, by wenzelm
tuned
2015-06-17, by nipkow
merged
2015-06-17, by nipkow
added funs and lemmas
2015-06-17, by nipkow
tuned proofs;
2015-06-17, by wenzelm
merged
2015-06-17, by wenzelm
manual merge;
2015-06-17, by wenzelm
tuned proofs;
2015-06-17, by wenzelm
isabelle update_cartouches;
2015-06-17, by wenzelm
avoid dynamic parsing of hardwired strings;
2015-06-17, by wenzelm
more compact name
2015-06-17, by nipkow
NEWS
2015-06-17, by nipkow
merged
2015-06-17, by nipkow
renamed Multiset.set_of to the canonical set_mset
2015-06-17, by nipkow
correccted the pretty-printing specs for setsum and setprod
2015-06-17, by paulson
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
2015-06-17, by paulson
another messy proof fixed
2015-06-16, by paulson
merged
2015-06-15, by wenzelm
more informative check: dummies are always allowed parse_term and should not lead to rejection here;
2015-06-15, by wenzelm
vacuous fact `TERM x`;
2015-06-15, by wenzelm
tuned signature;
2015-06-15, by wenzelm
inverted another messy proof
2015-06-15, by paulson
redundant: read = check o parse;
2015-06-15, by wenzelm
tuned;
2015-06-15, by wenzelm
moved sections;
2015-06-15, by wenzelm
moved sections;
2015-06-15, by wenzelm
tuned;
2015-06-15, by wenzelm
more robust: variables need not occur in body;
2015-06-15, by wenzelm
tuned;
2015-06-15, by wenzelm
tuned whitespace;
2015-06-15, by wenzelm
merged
2015-06-14, by wenzelm
improved treatment of Element.Obtains via Expression.prepare_stmt;
2015-06-14, by wenzelm
clarified context;
2015-06-14, by wenzelm
tuned comment;
2015-06-14, by wenzelm
another tangled proof
2015-06-14, by paulson
Merge
2015-06-14, by paulson
Tidied up more proofs
2015-06-14, by paulson
merged
2015-06-14, by wenzelm
more examples;
2015-06-14, by wenzelm
tuned signature;
2015-06-14, by wenzelm
tuned;
2015-06-14, by wenzelm
another proof
2015-06-14, by paulson
fixing more proofs
2015-06-14, by paulson
Merge
2015-06-13, by paulson
Merge
2015-06-13, by paulson
fixed another horrible proof
2015-06-13, by paulson
tuned proofs;
2015-06-13, by wenzelm
tuned signature;
2015-06-13, by wenzelm
merged
2015-06-13, by wenzelm
more on 'consider' and related concepts;
2015-06-13, by wenzelm
tuned proofs;
2015-06-13, by wenzelm
tuned proofs;
2015-06-13, by wenzelm
open parameters for 'consider' rule;
2015-06-13, by wenzelm
implicit rule for method "cases";
2015-06-13, by wenzelm
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
2015-06-13, by wenzelm
clarified 'obtain', using structured 'have' statement;
2015-06-13, by wenzelm
tuned comments;
2015-06-13, by wenzelm
clarified 'consider', using structured 'have' statement;
2015-06-13, by wenzelm
more examples;
2015-06-13, by wenzelm
renamed "prems" to "that";
2015-06-13, by wenzelm
support for 'consider' command;
2015-06-11, by wenzelm
made SML/NJ happy;
2015-06-11, by wenzelm
support to parse obtain clause without type-checking yet;
2015-06-11, by wenzelm
tuned -- eliminated unused feature;
2015-06-11, by wenzelm
tuned signature;
2015-06-11, by wenzelm
tuned;
2015-06-11, by wenzelm
streamlined many more proofs
2015-06-13, by paulson
Merge
2015-06-13, by paulson
tidied more proofs
2015-06-13, by paulson
proper subclass instances for existing gcd (semi)rings
2015-06-12, by haftmann
slight preference for American English
2015-06-12, by haftmann
generalized euclidean ring prerequisites
2015-06-12, by haftmann
simplified relationship between associated and is_unit
2015-06-12, by haftmann
proof tidying
2015-06-13, by paulson
CONTRIBUTORS
2015-06-12, by haftmann
tuned lemmas and proofs
2015-06-12, by haftmann
given up trivial definition
2015-06-12, by haftmann
dropped warnings by dropping ineffective code declarations
2015-06-12, by haftmann
standardized algebraic conventions: prefer a, b, c over x, y, z
2015-06-12, by haftmann
uniform _ div _ as infix syntax for ring division
2015-06-12, by haftmann
fixed several "inside-out" proofs
2015-06-11, by paulson
add transfer theorems for fixed points
2015-06-11, by hoelzl
Merge
2015-06-11, by paulson
tidied more proofs
2015-06-11, by paulson
misc tuning;
2015-06-10, by wenzelm
misc tuning;
2015-06-10, by wenzelm
unused;
2015-06-10, by wenzelm
misc tuning;
2015-06-10, by wenzelm
isabelle update_cartouches;
2015-06-10, by wenzelm
more user aliases;
2015-06-10, by wenzelm
merged
2015-06-10, by wenzelm
prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;
2015-06-10, by wenzelm
tuned proofs;
2015-06-10, by wenzelm
clarified local after_qed: result is not exported yet;
2015-06-10, by wenzelm
support for "if prems" in local goal statements;
2015-06-10, by wenzelm
tuned message;
2015-06-10, by wenzelm
tuned proofs;
2015-06-10, by wenzelm
no need for protected goal (see 240ad53041c9);
2015-06-10, by wenzelm
tuned proofs;
2015-06-10, by wenzelm
prevent export of future result -- avoid interference with goal fixes;
2015-06-10, by wenzelm
more uniform treatment of auto bindings vs. explicit user bindings;
2015-06-09, by wenzelm
tuned signature;
2015-06-09, by wenzelm
allow for_fixes for 'have', 'show' etc.;
2015-06-09, by wenzelm
eliminated dead code;
2015-06-09, by wenzelm
clarified abstracted term bindings (again, see c8384ff11711);
2015-06-09, by wenzelm
tuned signature;
2015-06-09, by wenzelm
tuned;
2015-06-09, by wenzelm
clarified term bindings;
2015-06-09, by wenzelm
tuned
2015-06-10, by fleury
Merge
2015-06-10, by Mathias Fleury
tuned
2015-06-10, by Mathias Fleury
Renaming multiset operators < ~> <#,...
2015-06-10, by Mathias Fleury
more tidying up of proofs
2015-06-09, by paulson
tidying messy proofs
2015-06-08, by paulson
tidying messy proofs
2015-06-08, by paulson
merged
2015-06-08, by wenzelm
clarified context;
2015-06-08, by wenzelm
tuned;
2015-06-08, by wenzelm
clarified abstracted term bindings;
2015-06-08, by wenzelm
avoid duplicate warning due to Variable.warn_extra_tfrees;
2015-06-08, by wenzelm
clarified Proof_Context.cert_propp/read_propp;
2015-06-08, by wenzelm
more careful treatment of term bindings in 'obtain' proof body;
2015-06-08, by wenzelm
tuned signature;
2015-06-08, by wenzelm
Merge
2015-06-08, by paulson
Tidied lots of messy proofs
2015-06-08, by paulson
tuned signature;
2015-06-07, by wenzelm
tuned (see also 66e6c539a36d);
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
clarified: declare props once and for all;
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
tuned signature;
2015-06-07, by wenzelm
tuned;
2015-06-07, by wenzelm
tuned;
2015-06-07, by wenzelm
tuned;
2015-06-07, by wenzelm
tuned whitespace;
2015-06-07, by wenzelm
more tight treatment of subgoals: main goal may refer to extra variables;
2015-06-06, by wenzelm
added Isar command 'supply';
2015-06-05, by wenzelm
tuned;
2015-06-05, by wenzelm
clarified signature -- better support for Isar commands outside of Pure;
2015-06-05, by wenzelm
merged
2015-06-03, by wenzelm
clarified context;
2015-06-03, by wenzelm
tuned;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
cleaified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
clarified context;
2015-06-02, by wenzelm
tuned proof;
2015-06-02, by wenzelm
merged
2015-06-03, by noschinl
simps_of_case: Better error if split rule is not an equality
2015-06-02, by noschinl
simps_of_case: allow Drule.dummy_thm as ignored split rule
2015-06-02, by noschinl
implicit partial divison operation in integral domains
2015-06-01, by haftmann
separate class for division operator, with particular syntax added in more specific classes
2015-06-01, by haftmann
explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
2015-06-01, by haftmann
dropped dead config option
2015-06-01, by haftmann
tuned, including proper signature for functor argument
2015-06-01, by haftmann
dropped dead code
2015-06-01, by haftmann
explicit argument expansion of uncheck rules;
2015-06-01, by haftmann
explicit input marker for operations
2015-06-01, by haftmann
completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
2015-06-01, by haftmann
self-contained formulation of abbrev for named targets
2015-06-01, by haftmann
correct sort constraints for abbreviations in type classes
2015-06-01, by haftmann
separate function to compute exported abbreviation
2015-06-01, by haftmann
clearly separated target primitives (target_foo) from self-contained target operations (foo)
2015-06-01, by haftmann
tuned order
2015-06-01, by haftmann
dedicated config options to deactivate uncheck phase for improvable syntax
2015-06-01, by haftmann
clarified interfaces for improvable syntax
2015-06-01, by haftmann
tuned
2015-06-01, by haftmann
clarified context;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
tuned;
2015-06-01, by wenzelm
discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
2015-06-01, by wenzelm
discontinued legacy;
2015-06-01, by wenzelm
obsolete (see 189c81779a68);
2015-06-01, by wenzelm
eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
tuned;
2015-06-01, by wenzelm
clarified context;
2015-06-01, by wenzelm
tuned;
2015-06-01, by wenzelm
obsolete;
2015-05-31, by wenzelm
clarified context;
2015-05-31, by wenzelm
tuned;
2015-05-31, by wenzelm
tuned;
2015-05-31, by wenzelm
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
2015-05-30, by wenzelm
tuned spelling;
2015-05-30, by wenzelm
unused;
2015-05-30, by wenzelm
tuned;
2015-05-30, by wenzelm
more explicit context;
2015-05-30, by wenzelm
obsolete;
2015-05-30, by wenzelm
tuned -- more direct Thm.renamed_prop;
2015-05-30, by wenzelm
tuned message;
2015-05-30, by wenzelm
tuned whitespace;
2015-05-30, by wenzelm
removed model checks from Nitpick
2015-05-29, by blanchet
document Nitpick issue
2015-05-29, by blanchet
uncountability: open interval equivalences
2015-05-29, by paulson
Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-28, by paulson
made Auto Sledgehammer behave more like the real thing
2015-05-28, by blanchet
took out Sledgehammer minimizer optimization that breaks things
2015-05-28, by blanchet
modernized (slightly) type compiler in MicroJava
2015-05-28, by kleing
New material about paths, and some lemmas
2015-05-26, by paulson
removed obsolete RC tags;
2015-05-25, by wenzelm
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-25, by wenzelm
Added tag Isabelle2015 for changeset 5ae2a2e74c93
2015-05-25, by wenzelm
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
Isabelle2015
2015-05-23, by wenzelm
updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;
2015-05-22, by wenzelm
tuned;
2015-05-22, by wenzelm
tuned;
2015-05-22, by wenzelm
updated versions;
2015-05-21, by wenzelm
tuned;
2015-05-21, by wenzelm
tuned;
2015-05-21, by wenzelm
cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;
2015-05-20, by wenzelm
more on displays with very high resolution;
2015-05-19, by wenzelm
add Haskabelle-2015 component
2015-05-18, by Lars Noschinski
Added tag Isabelle2015-RC5 for changeset d7f636331176
2015-05-17, by wenzelm
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
2015-05-17, by wenzelm
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
2015-05-17, by wenzelm
tuned;
2015-05-17, by wenzelm
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
2015-05-16, by wenzelm
clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
2015-05-13, by wenzelm
tuned whitespace;
2015-05-13, by wenzelm
more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;
2015-05-13, by wenzelm
Added tag Isabelle2015-RC4 for changeset 05fe9bdc4f8f
2015-05-09, by wenzelm
new CVC4 component
2015-05-09, by blanchet
took out unreliable 'blast' from tactic altogether
2015-05-09, by blanchet
clarified tooltip;
2015-05-08, by wenzelm
sledgehammer panel operation re-uses more of the Isar command, notably Try0.silence_methods to avoid spurious warnings intruding the document view;
2015-05-08, by wenzelm
more standard command setup;
2015-05-08, by wenzelm
silence local Unify.trace_bound as well: existing tools either refer to Proof.context or theory;
2015-05-08, by wenzelm
more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
2015-05-08, by wenzelm
use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
2015-05-07, by wenzelm
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
2015-05-07, by wenzelm
updated screenshot;
2015-05-06, by wenzelm
tuned;
2015-05-06, by wenzelm
less confusing default;
2015-05-06, by wenzelm
proper bib entry;
2015-05-06, by wenzelm
prevent incoherent default in SideKick 1.7;
2015-05-06, by wenzelm
corrected path in doc
2015-05-06, by blanchet
tuned;
2015-05-05, by wenzelm
more documentation;
2015-05-05, by wenzelm
more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
2015-05-05, by wenzelm
Added tag Isabelle2015-RC3 for changeset e0c3e11e9bea
2015-05-04, by wenzelm
tuned;
2015-05-04, by wenzelm
CONTRIBUTORS
2015-05-04, by kuncar
update isar-ref on Lifting
2015-05-04, by kuncar
NEWS
2015-05-04, by kuncar
tuned;
2015-05-04, by wenzelm
more on GTK;
2015-05-04, by wenzelm
more on Isabelle document preparation and bibtex files;
2015-05-04, by wenzelm
tuned spelling;
2015-05-04, by wenzelm
updated screenshot;
2015-05-03, by wenzelm
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
2015-05-03, by blanchet
made split-rule tactic go beyond constructors with 20 arguments
2015-05-03, by blanchet
proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;
2015-05-03, by wenzelm
tuned output to resemble input syntax more closely;
2015-05-03, by wenzelm
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
2015-05-03, by wenzelm
proper header;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output -- avoid empty quites and extra breaks;
2015-05-03, by wenzelm
tuned;
2015-05-03, by wenzelm
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
2015-05-03, by wenzelm
make SML/NJ more happy;
2015-05-03, by wenzelm
tuned message;
2015-05-03, by wenzelm
add testing file for code_dt extension of lifting
2015-05-02, by kuncar
handle error messages also in after_qed
2015-05-02, by kuncar
reorder some steps in the construction to support mutual datatypes
2015-05-02, by kuncar
more readable error message if some types do not correspond to sort constraints of the datatype
2015-05-02, by kuncar
better precomputing
2015-05-02, by kuncar
equivalence in code_dt data structure must respect both rty and qty
2015-05-02, by kuncar
don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
2015-05-02, by kuncar
go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
2015-04-13, by kuncar
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
2014-12-05, by kuncar
tuned proof; forget the transfer rule for size_fset
2014-12-05, by kuncar
return also which code equation was used; tuned
2014-12-05, by kuncar
publish lifting_forget and lifting_udpate interface
2014-12-05, by kuncar
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
2014-12-05, by kuncar
export the result of lifting_def
2014-11-18, by kuncar
useful function
2014-11-18, by kuncar
parametrize liting of terms by quotients
2014-11-18, by kuncar
improve handling of predicators in rsp_thm
2014-11-18, by kuncar
tuned; store pred_simps
2014-11-18, by kuncar
lift_definition: return the result of lifting
2014-11-18, by kuncar
lift_definition: interface also with tactic
2014-11-18, by kuncar
generalize prove_schematic_quot_thm
2014-11-18, by kuncar
added pred_def, rel_eq_onp tuned
2014-11-18, by kuncar
misc tuning, based on warnings by IntelliJ IDEA;
2015-05-03, by wenzelm
tuned;
2015-05-01, by wenzelm
updated screenshot;
2015-05-01, by wenzelm
clarified markup range;
2015-05-01, by wenzelm
modifier markup for all parsed tokens;
2015-05-01, by wenzelm
updated screenshots;
2015-05-01, by wenzelm
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
2015-04-30, by wenzelm
avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);
2015-04-30, by wenzelm
allow sorts on dead variables in BNFs
2015-04-28, by blanchet
tuned whitespace;
2015-04-28, by wenzelm
avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
2015-04-28, by wenzelm
code equations as displayable content in code dependency graph
2015-04-27, by wenzelm
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
2015-04-27, by wenzelm
added checkbox for try0;
2015-04-25, by wenzelm
made CVC4 support work also without unsat cores
2015-04-25, by blanchet
more paranoia settings, e.g. relevant for Ubuntu 15.04;
2015-04-24, by wenzelm
Added tag Isabelle2015-RC2 for changeset 8483c2883c8c
2015-04-24, by wenzelm
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
2015-04-24, by wenzelm
tuned;
2015-04-24, by wenzelm
tuned message, in accordance to ML side;
2015-04-24, by wenzelm
tuned settings to avoid sporadic crashes;
2015-04-24, by wenzelm
clarified settings for default Poly/ML version: test the actual Isabelle component;
2015-04-24, by wenzelm
avoid binding warning in Nitpick
2015-04-22, by blanchet
doc
2015-04-22, by blanchet
clarified permissions;
2015-04-22, by wenzelm
allow diagnostic proof commands with skip_proofs;
2015-04-22, by wenzelm
tuned signature;
2015-04-22, by wenzelm
updated polyml according to fixes-5.5.2 SVN version 2009;
2015-04-22, by wenzelm
declare Nitpick atoms to avoid '??.' prefixes in output
2015-04-20, by blanchet
proper isatest machine;
2015-04-19, by wenzelm
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
2015-05-23, by wenzelm
this warning is hardly useful but produces noisy markers in the jedit interface
2015-05-12, by nipkow
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
2015-05-09, by nipkow
generalized tends over powr; added DERIV rule for powr
2015-05-07, by hoelzl
added acknowledgment
2015-05-06, by blanchet
general Taylor series expansion with integral remainder
2015-05-05, by immler
generalized class constraints
2015-05-05, by immler
generalized differentiable_bound; some further variations of differentiable_bound
2015-05-05, by immler
moved basic lemmas about has_vector_derivative
2015-05-05, by immler
closures of intervals
2015-05-05, by immler
add lfp/gfp rule for nn_integral
2015-05-05, by hoelzl
strengthened lfp_ordinal_induct; added dual gfp variant
2015-05-04, by hoelzl
add rules for least/greatest fixed point calculus
2015-05-04, by hoelzl
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-05-04, by hoelzl
no more simp_legacy_precond
2015-05-04, by nipkow
no longer needed
2015-05-04, by nipkow
swap False to the right in assumptions to be eliminated at the right end
2015-05-03, by nipkow
merged
2015-05-01, by nipkow
simplified statement and proof
2015-05-01, by nipkow
tuned spelling;
2015-05-01, by wenzelm
Merge
2015-05-01, by paulson
Merge
2015-04-30, by paulson
Merge
2015-04-30, by paulson
tidying some messy proofs
2015-04-30, by paulson
new simp rule
2015-05-01, by nipkow
more formal source, more PIDE markup;
2015-04-30, by wenzelm
tuned -- avoid odd rebinding of "ctxt" and "context";
2015-04-30, by wenzelm
tuned;
2015-04-30, by wenzelm
use smaller example that fits into 64MB string limit of Poly/ML x86 platform;
2015-04-29, by wenzelm
tuned;
2015-04-29, by wenzelm
Tidying. Improved simplification for numerals, esp in exponents.
2015-04-29, by paulson
allow sorts on dead variables in BNFs
2015-04-28, by blanchet
added known bug
2015-04-28, by blanchet
tuning
2015-04-28, by blanchet
undid 6d7b7a037e8d
2015-04-28, by nipkow
New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-04-28, by paulson
Fixed a non-terminating proof (almost certainly caused by no change of mind)
2015-04-28, by paulson
new lemma
2015-04-27, by nipkow
new ==> simp rule
2015-04-25, by nipkow
improved docs
2015-04-22, by blanchet
merged
2015-04-22, by nipkow
merged
2015-04-22, by nipkow
added simp rules for ==>
2015-04-22, by nipkow
fixes for limits
2015-04-22, by paulson
New material, mostly about limits. Consolidation.
2015-04-21, by paulson
be less specific about POLYML_HOME, take component setup instead
2015-04-20, by kleing
declare Nitpick atoms to avoid '??.' prefixes in output
2015-04-20, by blanchet
back to post-release mode -- after fork point;
2015-04-19, by wenzelm
acknowledgment
2015-04-19, by blanchet
suppressed warnings
2015-04-19, by blanchet
updated docs, esp. relating to 'datatype_compat'
2015-04-19, by blanchet
typo
2015-04-19, by kleing
clarified keywords for quasi-command spans and Sidekick structure;
2015-04-18, by wenzelm
merged
2015-04-18, by wenzelm
tuned;
2015-04-18, by wenzelm
clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);
2015-04-18, by wenzelm
tweak afp mac options, try 64bit
2015-04-18, by kleing
compactified proposition
2015-04-17, by haftmann
merged
2015-04-17, by wenzelm
Added tag Isabelle2015-RC1 for changeset c9760373aa0f
2015-04-17, by wenzelm
tuned spelling;
2015-04-17, by wenzelm
sorted by automatic regeneration;
2015-04-17, by wenzelm
updated polyml according to fixes-5.5.2 SVN version 2007;
2015-04-17, by wenzelm
make SML/NJ happy;
2015-04-17, by wenzelm
just one line, to make it work with makedist_bundle;
2015-04-17, by wenzelm
merged
2015-04-17, by wenzelm
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
2015-04-17, by wenzelm
merged
2015-04-17, by Lars Noschinski
rewrite: work purely conversion-based
2015-04-17, by noschinl
ANNOUNCE material, based on NEWS;
2015-04-17, by wenzelm
tuned;
2015-04-17, by wenzelm
tuned for release;
2015-04-17, by wenzelm
merged;
2015-04-17, by wenzelm
finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
2015-04-17, by Rene Thiemann
(low importance) NEWS
2015-04-17, by traytel
merged
2015-04-17, by noschinl
merged
2015-04-17, by noschinl
rewrite: add default pattern "in concl" for more cases
2015-04-17, by noschinl
more session groups;
2015-04-17, by wenzelm
allow to exclude session groups;
2015-04-17, by wenzelm
merged
2015-04-17, by Lars Hupel
removed trivial lemmas
2015-04-16, by Lars Hupel
proper Theory.check;
2015-04-16, by wenzelm
make SML/NJ happy;
2015-04-16, by wenzelm
merged;
2015-04-16, by wenzelm
clarified document antiquotation: same check as in ML antiquotation;
2015-04-16, by wenzelm
formal Theory.check, with markup and completion;
2015-04-16, by wenzelm
tuned;
2015-04-16, by wenzelm
discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16, by wenzelm
tuned comment;
2015-04-16, by wenzelm
more explicit bootstrap_thy;
2015-04-16, by wenzelm
explicit error for Toplevel.proof_of;
2015-04-16, by wenzelm
clarified thy_deps;
2015-04-16, by wenzelm
tuned;
2015-04-16, by wenzelm
tuned signature;
2015-04-16, by wenzelm
misc tuning and clarification;
2015-04-16, by wenzelm
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
2015-04-16, by wenzelm
rewrite: use distinct names for unnamed abstractions
2015-04-16, by noschinl
avoid mix of languages;
2015-04-15, by wenzelm
merged
2015-04-15, by wenzelm
NEWS;
2015-04-15, by wenzelm
ensure that deps are defined in entries, to prevent crash of Graph_View.build_graph;
2015-04-15, by wenzelm
updated to jdk-7u80, the latest and last public release of Java 7;
2015-04-15, by wenzelm
session graph with folded base theories, as in document preparation;
2015-04-15, by wenzelm
tuned signature;
2015-04-15, by wenzelm
merged
2015-04-15, by noschinl
rewrite: add ML interface
2015-04-15, by noschinl
use wasysym for \<hole>;
2015-04-15, by wenzelm
tuned signature, clarified modules;
2015-04-15, by wenzelm
tuned messages;
2015-04-15, by wenzelm
obsolete (see also 94b2690ad494);
2015-04-15, by wenzelm
GUI controls for ML_statistics, for more digestible protocol dump;
2015-04-15, by wenzelm
more robust error handling of commands that are declared but not yet defined;
2015-04-15, by wenzelm
NEWS;
2015-04-14, by wenzelm
clarified sledgehammer options to approximate old-style diagnostic command;
2015-04-14, by wenzelm
prepared for more meta-simp rules (by Stefan Berghofer)
2015-04-14, by nipkow
merged
2015-04-14, by Andreas Lochbihler
add various lemmas about pmfs
2015-04-14, by Andreas Lochbihler
lemmas about integrals over bind and join on measures
2015-04-14, by Andreas Lochbihler
add lemmas
2015-04-14, by Andreas Lochbihler
generalise lemmas;
2015-04-14, by Andreas Lochbihler
add lemma about monotone convergence for countable integrals over arbitrary sequences
2015-04-14, by Andreas Lochbihler
add lemmas about restrict_space
2015-04-14, by Andreas Lochbihler
move lemma from AFP/Coinductive
2015-04-14, by Andreas Lochbihler
move some lemmas from AFP/Coinductive
2015-04-14, by Andreas Lochbihler
more lemmas about ereal
2015-04-14, by Andreas Lochbihler
more lemmas for cset
2015-04-14, by Andreas Lochbihler
add lemmas
2015-04-14, by Andreas Lochbihler
add lemmas
2015-04-14, by Andreas Lochbihler
merged
2015-04-14, by noschinl
rewrite: tuned code, no semantic changes
2015-04-14, by noschinl
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
2015-04-13, by noschinl
rewrite: do not descend into conclusion of premise with asm pattern
2015-04-13, by noschinl
rewrite: with asm pattern, try all premises for rewriting, not only the first
2015-04-13, by noschinl
tuned
2015-04-13, by noschinl
rewrite: propagate premises to new subgoals
2015-04-13, by noschinl
reformat comments
2015-04-13, by noschinl
rewr_cconv: ignore premises when tuning conclusion
2015-04-13, by noschinl
enable \<hole> syntax for rewrite
2015-04-13, by noschinl
call Goal.prove only once for a quadratic number of theorems
2015-04-13, by traytel
predicate compiler: ignore Abs_filter and Rep_filter
2015-04-13, by hoelzl
merged
2015-04-13, by nipkow
moved _aux functions from AFP/Collections to AList
2015-04-13, by nipkow
merged
2015-04-13, by hoelzl
replace Filters in NSA by HOL-Filters
2015-04-12, by hoelzl
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
2015-04-12, by hoelzl
add cofinite filter
2015-04-12, by hoelzl
add frequently as dual for eventually
2015-04-12, by hoelzl
add quantifier syntax for eventually
2015-04-12, by hoelzl
move filters to their own theory
2015-04-12, by hoelzl
fix latex in Transcendental
2015-04-12, by hoelzl
proper site for Cygwin setup;
2015-04-12, by wenzelm
less ambitious collection of quasi-generic PIDE modules;
2015-04-12, by wenzelm
tuned;
2015-04-12, by wenzelm
autorebase.bat.done no longer exists in Cygwin 1.7.35 -- lets hope that its incremental rebasing works for us;
2015-04-12, by wenzelm
merged
2015-04-12, by wenzelm
tuned -- avoid ML warnings;
2015-04-12, by wenzelm
avoid redundant shell process;
2015-04-12, by wenzelm
clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
2015-04-12, by wenzelm
Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]
2015-04-12, by paulson
tuned;
2015-04-12, by wenzelm
merged
2015-04-11, by wenzelm
proper Pretty.brk -- redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
2015-04-11, by wenzelm
tuned whitespace;
2015-04-11, by wenzelm
Merge
2015-04-11, by paulson
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
2015-04-11, by paulson
Merge
2015-04-11, by paulson
Merge
2015-04-11, by paulson
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-04-11, by paulson
updated for release;
2015-04-11, by wenzelm
updated for release;
2015-04-11, by wenzelm
Added tag Isabelle2015-RC0 for changeset 42d34eeb283c
2015-04-11, by wenzelm
more uniform Isabelle_System.mkdirs in ML/Scala;
2015-04-11, by wenzelm
updated for release;
2015-04-11, by wenzelm
tuned;
2015-04-11, by wenzelm
tuned spelling;
2015-04-11, by wenzelm
misc tuning for release;
2015-04-11, by wenzelm
make SML/NJ more happy;
2015-04-11, by wenzelm
make SML/NJ more happy;
2015-04-10, by wenzelm
tuned;
2015-04-10, by wenzelm
updated Cygwin near 1.7.35-1;
2015-04-10, by wenzelm
have 'primrec' return definitions
2015-04-10, by blanchet
renamed ML funs
2015-04-10, by blanchet
generalized code a bit
2015-04-10, by blanchet
generalized code
2015-04-10, by blanchet
exported function (for symmetry)
2015-04-10, by blanchet
merged
2015-04-10, by nipkow
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
2015-04-10, by nipkow
tuned proofs;
2015-04-10, by wenzelm
tuned signature;
2015-04-10, by wenzelm
tuned;
2015-04-10, by wenzelm
renamed misleading option
2015-04-09, by blanchet
obsolete;
2015-04-09, by wenzelm
make SML/NJ more happy;
2015-04-09, by wenzelm
merged
2015-04-09, by wenzelm
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-09, by wenzelm
tuned signature
2015-04-09, by blanchet
fixed typo in function name
2015-04-09, by blanchet
removed a refute example that caused trouble with testing
2015-04-09, by blanchet
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
2015-04-09, by blanchet
merged
2015-04-09, by haftmann
conversion between division on nat/int and division in archmedean fields
2015-04-09, by haftmann
replace almost_everywhere_zero by Infinite_Set.MOST
2015-04-09, by hoelzl
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
2015-04-09, by wenzelm
tuned signature;
2015-04-09, by wenzelm
misc tuning for release;
2015-04-08, by wenzelm
merged
2015-04-08, by wenzelm
eliminated suspicious Unicode character;
2015-04-08, by wenzelm
eliminated hard tabs;
2015-04-08, by wenzelm
more standard access to goal state;
2015-04-08, by wenzelm
more standard Isabelle/ML tool setup;
2015-04-08, by wenzelm
added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);
2015-04-08, by wenzelm
proper test for session HOL-Library;
2015-04-08, by wenzelm
tuned;
2015-04-08, by wenzelm
tuned signature;
2015-04-08, by wenzelm
proper context for Object_Logic operations;
2015-04-08, by wenzelm
explicitly checked alpha conversion -- actual renaming happens outside kernel;
2015-04-08, by wenzelm
more standard access to specific subgoal;
2015-04-08, by wenzelm
tuned wording
2015-04-08, by blanchet
updated 'old_smt' to loss of 'z3_non_commercial' option
2015-04-08, by blanchet
Z3 news
2015-04-08, by blanchet
updated certificates to latest Z3 (and took out one problem that no longer works)
2015-04-08, by blanchet
updated docs to reflect actually run ATPs
2015-04-08, by blanchet
reorder provers to reflect current eval results
2015-04-08, by blanchet
updated docs to Z3 open source
2015-04-08, by blanchet
updated SMT module and Sledgehammer to fully open source Z3
2015-04-08, by blanchet
updated to new Z3
2015-04-08, by blanchet
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
2015-04-08, by blanchet
removed TODO
2015-04-08, by blanchet
consistent naming
2015-04-08, by Andreas Lochbihler
merged
2015-04-08, by Andreas Lochbihler
more lemmas and operations on cset (adapted from FSet)
2015-04-08, by Andreas Lochbihler
tuned signature;
2015-04-08, by wenzelm
tuned;
2015-04-08, by wenzelm
misc tuning for release;
2015-04-08, by wenzelm
merged
2015-04-07, by nipkow
Removed mcard because it is equal to size
2015-04-07, by nipkow
generalized slightly
2015-04-07, by blanchet
generalized code
2015-04-07, by blanchet
generalized code
2015-04-07, by blanchet
export ML function
2015-04-07, by blanchet
recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
2015-04-07, by wenzelm
more qualified names -- eliminated hide_const (open);
2015-04-07, by wenzelm
tuned;
2015-04-06, by wenzelm
merged
2015-04-06, by wenzelm
local setup of induction tools, with restricted access to auxiliary consts;
2015-04-06, by wenzelm
support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-06, by wenzelm
tuned;
2015-04-06, by wenzelm
clarified rail syntax;
2015-04-06, by wenzelm
@{command_spec} is superseded by @{command_keyword};
2015-04-06, by wenzelm
clarified command keyword markup;
2015-04-06, by wenzelm
more position information and PIDE markup for command keywords;
2015-04-06, by wenzelm
allow prefix before keyword, notably 'private';
2015-04-06, by wenzelm
support local command setup;
2015-04-06, by wenzelm
proper header;
2015-04-06, by wenzelm
tuned signature;
2015-04-06, by wenzelm
tuned;
2015-04-06, by wenzelm
new theory Library/Tree_Multiset.thy
2015-04-06, by nipkow
more standard local_theory command setup;
2015-04-04, by wenzelm
some explanation of 'private';
2015-04-04, by wenzelm
tuned message;
2015-04-04, by wenzelm
more general notion of command span: command keyword not necessarily at start;
2015-04-04, by wenzelm
support private scope for individual local theory commands;
2015-04-04, by wenzelm
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
2015-04-03, by wenzelm
obsolete (see 8b7caf447357);
2015-04-03, by wenzelm
check wrt. proper context, e.g. relevant for 'experiment' target;
2015-04-03, by wenzelm
clarified name space policy: show less stuff in usual print functions;
2015-04-03, by wenzelm
unused;
2015-04-03, by wenzelm
more uniform "verbose" option to print name space;
2015-04-03, by wenzelm
tuned;
2015-04-03, by wenzelm
merged
2015-04-02, by wenzelm
proper treatment of internal method name as already checked Token.src;
2015-04-02, by wenzelm
tuned signature;
2015-04-02, by wenzelm
export for informative purposes;
2015-04-02, by wenzelm
sort constraints are inherent part of class abbreviations (in contrast to class constants)
2015-04-02, by haftmann
semidom contains distributive minus, by convention
2015-04-02, by haftmann
clarified method_closure;
2015-04-02, by wenzelm
operation on embedded sources for Eisbach;
2015-04-02, by wenzelm
tuned signature;
2015-04-02, by wenzelm
tuned -- emphasize semantics of already checked src;
2015-04-02, by wenzelm
misc tuning -- keep name space more clean;
2015-04-01, by wenzelm
tuned;
2015-04-01, by wenzelm
merged
2015-04-01, by wenzelm
misc tuning -- keep name space more clean;
2015-04-01, by wenzelm
added command 'experiment';
2015-04-01, by wenzelm
imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;
2015-04-01, by wenzelm
NEWS;
2015-04-01, by wenzelm
clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
2015-04-01, by wenzelm
evade popular keyword;
2015-04-01, by wenzelm
tuned signature;
2015-04-01, by wenzelm
clarified module;
2015-04-01, by wenzelm
ISABELLE_JAVA_SYSTEM_OPTIONS for scala REPL;
2015-04-01, by wenzelm
more reactive interrupts;
2015-04-01, by wenzelm
added isabelle build option -x, to exclude sessions;
2015-04-01, by wenzelm
added isabelle build option -k, for fast off-line checking of theory sources;
2015-04-01, by wenzelm
tuned signature;
2015-04-01, by wenzelm
tuned message;
2015-04-01, by wenzelm
tuned signature;
2015-04-01, by wenzelm
more visibility flags on background naming;
2015-03-31, by wenzelm
support for explicit scope of private entries;
2015-03-31, by wenzelm
subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
2015-03-31, by wenzelm
tuned signature;
2015-03-31, by wenzelm
tuned signature;
2015-03-31, by wenzelm
tuned -- avoid exotic Name_Space.defined_entry;
2015-03-31, by wenzelm
tuned;
2015-03-31, by wenzelm
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-31, by wenzelm
tuned;
2015-03-31, by wenzelm
tuned message;
2015-03-31, by wenzelm
more standard Long_Name operations;
2015-03-31, by wenzelm
tuned;
2015-03-31, by wenzelm
tuned;
2015-03-31, by wenzelm
tuned signature;
2015-03-31, by wenzelm
simplified code
2015-04-01, by blanchet
Theorem "arctan" is no longer a default simprule
2015-04-01, by paulson
John Harrison's example: a 32-bit approximation to pi. SLOW
2015-04-01, by paulson
HOL Light Libraries for complex Arctan, Arcsin, Arccos
2015-04-01, by paulson
arcsin and arccos lemmas
2015-04-01, by paulson
NEWS
2015-03-31, by haftmann
given up separate type classes demanding `inverse 0 = 0`
2015-03-31, by haftmann
Merge
2015-03-31, by paulson
rationalised and generalised some theorems concerning abs and x^2.
2015-03-31, by paulson
added lemmas
2015-03-31, by nipkow
Merge
2015-03-31, by paulson
New material and binomial fix
2015-03-31, by paulson
tuned doc
2015-03-31, by blanchet
merged
2015-03-31, by wenzelm
tuned signature;
2015-03-31, by wenzelm
support for strictly private name space entries;
2015-03-30, by wenzelm
tuned signature;
2015-03-30, by wenzelm
export more low-level theorems in data structure (partly for 'corec')
2015-03-30, by blanchet
tuned;
2015-03-30, by wenzelm
merged
2015-03-30, by wenzelm
more uniform syntax for named instantiations;
2015-03-30, by wenzelm
merged
2015-03-30, by hoelzl
added locale for semirings
2015-03-30, by Rene Thiemann
exposed approximation in ML
2015-03-30, by eberlm
clarified NEWS (cf. 97872c658a44);
2015-03-30, by wenzelm
clarified equality of formal entities;
2015-03-29, by wenzelm
merged
2015-03-29, by wenzelm
tuned signature;
2015-03-29, by wenzelm
ind_cases: clarified preparation of arguments;
2015-03-29, by wenzelm
support for minimal specifications, with usual treatment of fixes and dummies;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
tuned signature;
2015-03-29, by wenzelm
proper local Proof_Context.arity_sorts;
2015-03-29, by wenzelm
more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;
2015-03-29, by wenzelm
avoid low-level tsig operations;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
clarified context;
2015-03-29, by wenzelm
rule_insts_schematic is considered legacy and false by default;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
clarified no_zero_devisors: makes only sense in a semiring;
2015-03-28, by haftmann
dropped long-outdated comments
2015-03-28, by haftmann
merged
2015-03-28, by wenzelm
clarified goal context;
2015-03-28, by wenzelm
clarified goal context;
2015-03-28, by wenzelm
prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
2015-03-28, by wenzelm
proper Rule_Insts.read_term, e.g. to enable case_tac using "_";
2015-03-27, by wenzelm
tuned signature;
2015-03-27, by wenzelm
clarified goal context;
2015-03-27, by wenzelm
clarified doc
2015-03-27, by blanchet
more graceful failure if some of the involved BNFs have no data
2015-03-27, by blanchet
sort BNFs in output
2015-03-27, by blanchet
preserve order of type arguments in pre-FP BNF typedef
2015-03-27, by blanchet
register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')
2015-03-26, by blanchet
store low-level (un)fold constants
2015-03-26, by blanchet
export more functions
2015-03-26, by blanchet
restored broken metis proof
2015-03-26, by haftmann
distributivity of partial minus establishes desired properties of dvd in semirings
2015-03-23, by haftmann
explicit commutative additive inverse operation;
2015-03-23, by haftmann
modernized
2015-03-23, by haftmann
more multiset theorems
2015-03-25, by blanchet
semantic completion for @{system_option};
2015-03-25, by wenzelm
clarified position;
2015-03-25, by wenzelm
HOL-SPARK .prv files are subject to system option spark_prv;
2015-03-25, by wenzelm
tuned signature;
2015-03-25, by wenzelm
NEWS;
2015-03-25, by wenzelm
prefer local fixes;
2015-03-25, by wenzelm
proper signature;
2015-03-25, by wenzelm
dummies may depend on goal params as well;
2015-03-25, by wenzelm
merged
2015-03-24, by wenzelm
proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;
2015-03-24, by wenzelm
clarified case_tac fixes and context;
2015-03-24, by wenzelm
clarified name;
2015-03-24, by wenzelm
option to control old-style schematic mode;
2015-03-24, by wenzelm
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
2015-03-24, by wenzelm
tuned;
2015-03-24, by wenzelm
tuned proof;
2015-03-24, by wenzelm
admit dummy patterns in instantiations;
2015-03-24, by wenzelm
clarified input source;
2015-03-24, by wenzelm
tuning
2015-03-24, by blanchet
reordered properties
2015-03-24, by blanchet
NEWS;
2015-03-23, by wenzelm
tuned proof;
2015-03-23, by wenzelm
implicit goal parameters are improper;
2015-03-23, by wenzelm
merged
2015-03-23, by wenzelm
prefer local fixes;
2015-03-23, by wenzelm
local fixes may depend on goal params;
2015-03-23, by wenzelm
tuned;
2015-03-23, by wenzelm
clarified syntax category "fixes";
2015-03-23, by wenzelm
tuned signature;
2015-03-23, by wenzelm
tuned syntax diagrams -- no duplication of "target";
2015-03-23, by wenzelm
tuned;
2015-03-23, by wenzelm
tuned;
2015-03-23, by wenzelm
support 'for' fixes in rule_tac etc.;
2015-03-23, by wenzelm
fix parameter order of NO_MATCH
2015-03-23, by hoelzl
add measurable_submarkov
2015-03-23, by hoelzl
BT subsumed by Library/Tree
2015-03-23, by nipkow
added funs and lemmas
2015-03-23, by nipkow
tuned;
2015-03-22, by wenzelm
tuned;
2015-03-22, by wenzelm
tuned;
2015-03-22, by wenzelm
tuned;
2015-03-20, by wenzelm
read instantiations uniformly for rules and tactics;
2015-03-20, by wenzelm
removed presumably pointless detail;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
make SML/NJ happy;
2015-03-20, by wenzelm
Merge
2015-03-20, by paulson
tweaked a few slow or very ugly proofs
2015-03-20, by paulson
merged
2015-03-20, by wenzelm
tuned signature;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
tuned signature;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
tuned -- prepare instantiation more uniformly;
2015-03-20, by wenzelm
Merge
2015-03-20, by paulson
fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
2015-03-20, by paulson
merged
2015-03-19, by wenzelm
more position information;
2015-03-19, by wenzelm
misc tuning;
2015-03-19, by wenzelm
tuned;
2015-03-19, by wenzelm
Merge
2015-03-19, by paulson
New material for complex sin, cos, tan, Ln, also some reorganisation
2015-03-19, by paulson
updated to sumatra_pdf-3.0;
2015-03-19, by wenzelm
tuned comments;
2015-03-19, by wenzelm
slightly more formal historic examples;
2015-03-19, by wenzelm
bounded powerset
2015-03-18, by traytel
new HOL Light material about exp, sin, cos
2015-03-18, by paulson
new file for complex transcendental functions
2015-03-18, by paulson
Merge
2015-03-18, by paulson
Merge
2015-03-18, by paulson
Merge
2015-03-18, by paulson
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-18, by paulson
merged
2015-03-18, by noschinl
added proof method rewrite
2015-03-18, by noschinl
merged
2015-03-18, by wenzelm
tuned;
2015-03-17, by wenzelm
tight span for theory header, which is relevant for error positions (including semantic completion);
2015-03-17, by wenzelm
misc tuning and simplification;
2015-03-17, by wenzelm
Inserted real_of_nat to fix factorial-related problem
2015-03-17, by paulson
more general type class for factorial. Now allows code generation (?)
2015-03-17, by paulson
Merge
2015-03-17, by paulson
Merge
2015-03-17, by paulson
The factorial function, "fact", now has type "nat => 'a"
2015-03-16, by paulson
merged
2015-03-17, by nipkow
added lemmas
2015-03-17, by nipkow
document property
2015-03-16, by traytel
BNF relators preserve reflexivity
2015-03-16, by traytel
export more ML functions
2015-03-16, by blanchet
merged
2015-03-16, by wenzelm
suppress semantic completion in errors of batch build -- avoid junk in log files;
2015-03-16, by wenzelm
updated docs
2015-03-16, by blanchet
clarified documentation
2015-03-16, by blanchet
proper headers;
2015-03-16, by wenzelm
merged
2015-03-16, by wenzelm
tuned message -- include completion;
2015-03-16, by wenzelm
support for completion reports produced in Scala (inlined into messages);
2015-03-16, by wenzelm
more precises positions;
2015-03-16, by wenzelm
avoid duplicate header errors, more precise positions;
2015-03-16, by wenzelm
tuned protocol -- resolve command positions in ML;
2015-03-16, by wenzelm
clarified modules;
2015-03-16, by wenzelm
add inequalities (move from AFP/Amortized_Complexity)
2015-03-16, by hoelzl
merge
2015-03-15, by blanchet
inlining threshold
2015-03-15, by blanchet
avoid controversial Pirate syntax
2015-03-15, by blanchet
more markup, which helps to create missing imports;
2015-03-15, by wenzelm
tuned signature;
2015-03-15, by wenzelm
proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-15, by wenzelm
clarified span position;
2015-03-15, by wenzelm
tuned;
2015-03-15, by wenzelm
tuned;
2015-03-15, by wenzelm
hybrid use of command blobs: inlined errors and auxiliary files;
2015-03-15, by wenzelm
more command categories, as in ML;
2015-03-15, by wenzelm
more command categories, as in ML;
2015-03-15, by wenzelm
tuned;
2015-03-15, by wenzelm
value-oriented user error, for well-defined Thy_Syntax.chop_common;
2015-03-14, by wenzelm
more explicit exception User_Error, with value-oriented equality;
2015-03-14, by wenzelm
tuned signature;
2015-03-14, by wenzelm
clarified positions of theory imports;
2015-03-14, by wenzelm
misc tuning -- more uniform ML vs. Scala;
2015-03-14, by wenzelm
tunes signature -- more uniform ML vs. Scala;
2015-03-14, by wenzelm
position parser as in ML;
2015-03-14, by wenzelm
tuned signature;
2015-03-13, by wenzelm
rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
2015-03-13, by nipkow
simplified Command.resolve_files in ML, using blobs_index from Scala;
2015-03-13, by wenzelm
removed junk;
2015-03-13, by wenzelm
tuned;
2015-03-13, by wenzelm
merged
2015-03-12, by wenzelm
clarified markup for embedded files, early before execution;
2015-03-12, by wenzelm
clarified command content;
2015-03-12, by wenzelm
tuned -- more uniform ML vs. Scala;
2015-03-12, by wenzelm
quote "method" to allow Eisbach using this keyword;
2015-03-12, by wenzelm
rel_pmf on equivalence relation
2015-03-12, by hoelzl
make proofs work with 4762c690a75c
2015-03-12, by Andreas Lochbihler
add subadditivity for Liminf on ereal
2015-03-11, by hoelzl
merged
2015-03-11, by Andreas Lochbihler
merged
2015-03-10, by Andreas Lochbihler
more type class instances
2015-03-10, by Andreas Lochbihler
documented renamed theories
2015-03-10, by blanchet
export more functions (for future 'corec')
2015-03-10, by blanchet
tuning
2015-03-10, by blanchet
merged
2015-03-10, by wenzelm
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-03-10, by wenzelm
generalized bind_cond_pmf_cancel
2015-03-10, by hoelzl
renaming HOL/Fact.thy -> Binomial.thy
2015-03-10, by paulson
Merge
2015-03-10, by paulson
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-03-10, by paulson
clarified Token.check_src: intern at most once;
2015-03-10, by wenzelm
add set_pmf lemmas to simpset
2015-03-10, by hoelzl
build pmf's on bind
2015-03-10, by hoelzl
split into subgoals
2015-03-10, by blanchet
tuning
2015-03-10, by blanchet
merged
2015-03-09, by wenzelm
support structural composition (THEN_ALL_NEW) for proof methods;
2015-03-09, by wenzelm
Removed the infix operator "choose" to allow HOLCF to build
2015-03-09, by paulson
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2015-03-09, by paulson
eliminated unused arith "verbose" flag -- tools that need options can use the context;
2015-03-09, by wenzelm
eliminated dead code (cf. 5e5c36b051af);
2015-03-09, by wenzelm
tuned;
2015-03-09, by wenzelm
clarified aliases;
2015-03-08, by wenzelm
misc tuning and simplification;
2015-03-08, by wenzelm
tuned;
2015-03-08, by wenzelm
misc tuning and simplification;
2015-03-08, by wenzelm
tuned;
2015-03-08, by wenzelm
cartouche_declaration for Eisbach;
2015-03-08, by wenzelm
NEWS;
2015-03-07, by wenzelm
clarified Drule.gen_all: observe context more carefully;
2015-03-07, by wenzelm
added declare_maxidx operations for Eisbach;
2015-03-07, by wenzelm
clarified Variable.export: observe maxidx of target context;
2015-03-07, by wenzelm
tuned;
2015-03-07, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
proper context;
2015-03-06, by wenzelm
tuned;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
updated to scala-2.11.6;
2015-03-06, by wenzelm
Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06, by wenzelm
merged
2015-03-06, by wenzelm
merged
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
tuned -- more explicit use of context;
2015-03-06, by wenzelm
tuned -- more explicit use of context;
2015-03-05, by wenzelm
A few new lemmas and a bit of tidying up
2015-03-06, by paulson
Merge
2015-03-05, by paulson
The function frac. Various lemmas about limits, series, the exp function, etc.
2015-03-05, by paulson
avoid needless 'if ... undefined' in generated theorems
2015-03-05, by blanchet
strengthened tactic
2015-03-05, by blanchet
strengthened tactic
2015-03-05, by blanchet
deal better with corecursion through functions
2015-03-05, by blanchet
removed too strict checks
2015-03-05, by blanchet
message tuning
2015-03-05, by blanchet
tuning
2015-03-05, by blanchet
improved primcorec messages
2015-03-05, by blanchet
improved primcorec messages
2015-03-05, by blanchet
better primcorec messages
2015-03-05, by blanchet
more primcorec messages
2015-03-05, by blanchet
more precise primcorec messages
2015-03-05, by blanchet
more precise primcorec messages
2015-03-05, by blanchet
better primcorec messages
2015-03-05, by blanchet
more 'primcorec' error handling
2015-03-05, by blanchet
helpful error message when 'auto' fails
2015-03-05, by blanchet
no quick_and_dirty for goals that may fail + tuned messages
2015-03-05, by blanchet
tuned new primrec messages
2015-03-05, by blanchet
reworked primcorec error messages
2015-03-05, by blanchet
fix import path
2015-03-05, by hoelzl
merged
2015-03-04, by wenzelm
tuned signature;
2015-03-04, by wenzelm
tuned signature;
2015-03-04, by wenzelm
removed unused;
2015-03-04, by wenzelm
merged
2015-03-04, by nipkow
Removed the obsolete functions "natfloor" and "natceiling"
2015-03-04, by nipkow
clarified signature;
2015-03-04, by wenzelm
tuned;
2015-03-04, by wenzelm
tuned;
2015-03-04, by wenzelm
merged;
2015-03-04, by wenzelm
tuned signature -- prefer qualified names;
2015-03-04, by wenzelm
alist is a BNF
2015-03-04, by traytel
eliminated some clones of Proof_Context.cterm_of
2015-03-03, by traytel
updated docs
2015-03-03, by blanchet
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"
2015-03-03, by blanchet
SPASS-Pirate is now called Pirate
2015-03-03, by blanchet
avoid duplicate simp warning for datatypes with explicit products
2015-03-03, by blanchet
removed needless (and inconsistent) qualifier that messes up with Mirabelle
2015-03-03, by blanchet
import 'Main' to be on the safe side
2015-03-03, by blanchet
added Proof_Context.cterm_of/ctyp_of convenience;
2015-03-01, by wenzelm
tuned;
2015-03-01, by wenzelm
updated to jedit-5.2.0;
2015-02-28, by wenzelm
spelling
2015-02-28, by haftmann
tuned whitespace;
2015-02-27, by wenzelm
typo
2015-02-26, by nipkow
tuned;
2015-02-24, by wenzelm
updated CVC4 component to include libgmp on Mac OS X
2015-02-24, by blanchet
more uniform headless mode for all derivatives of "build" (amending df5dc24ca712);
2015-02-23, by wenzelm
Goal.prove_multi is superseded by the fully general Goal.prove_common;
2015-02-23, by wenzelm
proper LaTeX;
2015-02-23, by wenzelm
make SML/NJ more happy;
2015-02-23, by wenzelm
added new tree material
2015-02-21, by nipkow
generalised the results by Eberl
2015-02-20, by paulson
more canonical order of subscriptions avoids superfluous facts
2015-02-19, by haftmann
got rid of linordered_field_class.sign_simps(41) !
2015-02-19, by paulson
establish unique preferred fact names
2015-02-19, by haftmann
eliminated technical fact alias
2015-02-18, by haftmann
eliminated fact duplicates
2015-02-18, by haftmann
inlined rules to free user-space from technical names
2015-02-18, by haftmann
explicit declaration allows cumulative declaration
2015-02-18, by haftmann
use more permissive logic for CVC4 (in case both reals and datatypes appear)
2015-02-17, by blanchet
deleted ineffective declarations
2015-02-15, by haftmann
dropped unused rules
2015-02-15, by haftmann
more direct expression of syntactic function records
2015-02-15, by haftmann
self-contained declaration attribute
2015-02-15, by haftmann
simpset with no redundancy
2015-02-15, by haftmann
times_divide_eq rules are already [simp] despite of comment
2015-02-15, by haftmann
explicit equivalence for strict order on lattices
2015-02-15, by haftmann
tuned
2015-02-15, by haftmann
purge variables not mentioned in body from pattern
2015-02-15, by haftmann
only collapse patterns with disjunctive variable names
2015-02-14, by haftmann
clarified
2015-02-14, by haftmann
avoid unused arguments
2015-02-14, by haftmann
tuned
2015-02-14, by haftmann
more consistent teminology
2015-02-14, by haftmann
fact consolidation
2015-02-14, by haftmann
dropped redundancy
2015-02-14, by haftmann
less warnings
2015-02-14, by haftmann
merged
2015-02-13, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context and method setup;
2015-02-11, by wenzelm
new lemmas re refinement of one equivalence relation WRT another
2015-02-12, by paulson
rel_pmf preserves orders
2015-02-11, by Andreas Lochbihler
generalise lemma
2015-02-11, by Andreas Lochbihler
more lemmas
2015-02-11, by Andreas Lochbihler
merged
2015-02-11, by Andreas Lochbihler
more transfer rules
2015-02-11, by Andreas Lochbihler
add lemmas about functions on option
2015-02-11, by Andreas Lochbihler
tuned proof
2015-02-11, by Andreas Lochbihler
add lema about card and vimage
2015-02-11, by Andreas Lochbihler
add more general version of finite_vimageD
2015-02-11, by Andreas Lochbihler
add lemma
2015-02-11, by Andreas Lochbihler
add lemmas about flat_ord
2015-02-11, by Andreas Lochbihler
add parametricity rules for monotone, fun_lub, and fun_ord
2015-02-11, by Andreas Lochbihler
add parametricity rule for Ex1
2015-02-11, by Andreas Lochbihler
add intro and elim rules for right_total
2015-02-11, by Andreas Lochbihler
add monotonicity lemmas for rel_fun
2015-02-11, by Andreas Lochbihler
add lemmas about bind and image
2015-02-11, by Andreas Lochbihler
updated NEWS
2015-02-11, by blanchet
updated Sledgehammer docs
2015-02-11, by blanchet
added CVC4 component (and took out CVC3 from main components)
2015-02-11, by blanchet
tuned default provers
2015-02-11, by blanchet
Merge
2015-02-11, by paulson
Not a simprule, as it complicates proofs
2015-02-10, by paulson
Merge
2015-02-10, by paulson
New lemmas and a bit of tidying up.
2015-02-10, by paulson
check unused theory;
2015-02-10, by wenzelm
tuned;
2015-02-10, by wenzelm
more accurate context;
2015-02-10, by wenzelm
merged
2015-02-10, by wenzelm
misc tuning;
2015-02-10, by wenzelm
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2015-02-10, by wenzelm
indicate slow proof (approx. 20s);
2015-02-10, by wenzelm
merged
2015-02-10, by hoelzl
add bind_cond_pmf_cancel
2015-02-10, by hoelzl
add cond_map_pmf
2015-02-10, by hoelzl
introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
2015-02-10, by hoelzl
tuned proof
2015-02-10, by Andreas Lochbihler
add another lemma to split nn_integral over product count_space
2015-02-10, by Andreas Lochbihler
tune proof
2015-02-10, by Andreas Lochbihler
nn_integral can be split over arbitrary product count_spaces
2015-02-10, by Andreas Lochbihler
add stronger version of lemma
2015-02-10, by Andreas Lochbihler
default abstypes and default abstract equations make technical (no_code) annotation superfluous
2015-02-06, by haftmann
careful about visibility of facts that have the same 'theory' in optimization
2015-02-06, by blanchet
non-intrusive default code setup for mappings
2015-02-06, by haftmann
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
2015-02-05, by haftmann
explicit type annotation avoids problems with Haskell type inference
2015-02-05, by haftmann
more explicit hint on import order
2015-02-05, by haftmann
dropped dead code;
2015-02-05, by haftmann
dropped obsolete external entrance point
2015-02-05, by haftmann
explicit error message for non-existing targets
2015-02-05, by haftmann
fixed typos
2015-02-02, by blanchet
less confusing constant
2015-02-02, by blanchet
tuning
2015-02-02, by blanchet
simp rules for return_pmf
2015-01-30, by hoelzl
related permutations with bij functions
2015-01-30, by hoelzl
canonical name
2015-01-30, by nipkow
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2015-01-29, by wenzelm
more explicit indication of Async_Manager_Legacy as Proof General legacy;
2015-01-29, by wenzelm
tuned bootstrap;
2015-01-29, by wenzelm
tuned;
2015-01-29, by wenzelm
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
2015-01-29, by wenzelm
unused;
2015-01-29, by wenzelm
ensure that running into older execution is interruptible (see also b91dc7ab3464);
2015-01-29, by wenzelm
clarified worker_wait;
2015-01-29, by wenzelm
explicit headless mode for machines that lack X11 (e.g. lxbroy10);
2015-01-28, by wenzelm
more robust protocol command: purge removed execs asynchronously, to remain reactive despite problems to cancel "Command.run_process" in a situation of overrunning non-terminating tasks (see also 59f1591a11cb);
2015-01-28, by wenzelm
tuned signature;
2015-01-28, by wenzelm
tuned comment;
2015-01-28, by wenzelm
tuned signature;
2015-01-28, by wenzelm
clarified module name;
2015-01-28, by wenzelm
abstract code equation may also be default
2015-01-28, by haftmann
proper term_of for iarray
2015-01-28, by haftmann
string printing conformant to both (S)ML and Isabelle/ML
2015-01-28, by haftmann
Fixed bug in bugfix for function package
2015-01-28, by eberlm
Fixed variable naming bug in function package
2015-01-28, by eberlm
moved bcontfun from AFP/Ordinary_Differential_Equations
2015-01-28, by hoelzl
ereal: tuned proofs concerning continuity and suprema
2015-01-27, by hoelzl
spelling error
2015-01-26, by hoelzl
NEWS;
2015-01-26, by wenzelm
removed unused operations;
2015-01-26, by wenzelm
prefer plain session_graph.pdf over GraphBrowser applet;
2015-01-26, by wenzelm
complete pattern coverage, e.g. relevant for singleton graph;
2015-01-26, by wenzelm
discontinued obsolete option "document_graph";
2015-01-25, by wenzelm
provide session_graph.pdf via Isabelle/Scala;
2015-01-25, by wenzelm
support for session graph from Scala side;
2015-01-25, by wenzelm
support for off-line graph output, without GUI thread;
2015-01-25, by wenzelm
make it independent from GUI thread, e.g. for Graph_File.write;
2015-01-25, by wenzelm
separate module Graph_File;
2015-01-25, by wenzelm
tuned comments;
2015-01-25, by wenzelm
tuned;
2015-01-25, by wenzelm
more compact message;
2015-01-25, by wenzelm
proper naming convention;
2015-01-25, by wenzelm
prefer plain tuples;
2015-01-25, by wenzelm
tuned message;
2015-01-25, by wenzelm
tuned;
2015-01-25, by wenzelm
tuned signature;
2015-01-24, by wenzelm
tuned;
2015-01-24, by wenzelm
tuned message;
2015-01-24, by wenzelm
more direct Output.output;
2015-01-24, by wenzelm
avoid newline in Pretty.str;
2015-01-24, by wenzelm
merged
2015-01-23, by Andreas Lochbihler
generalise lemma
2015-01-23, by Andreas Lochbihler
integral of the product of count spaces equals the integral of the count space of the product type
2015-01-23, by hoelzl
import general thms from Density_Compiler
2015-01-22, by hoelzl
backout cefeea956989: Graphview *is* required in Pure to replace old browser eventually;
2015-01-22, by wenzelm
backed out obsolete workaround from ef1edfb36af7
2015-01-22, by haftmann
disjunctive bottom and supremum lists
2015-01-21, by haftmann
sufficent to have graphview as part of jEdit rather than Pure
2015-01-21, by haftmann
option for formally inlined class specifications in hierarchy graph
2015-01-21, by haftmann
clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
2015-01-21, by wenzelm
updated to jdk-7u76, which appears to be more stable than jdk-8u31 (e.g. crashes jEdit/Console plugin of Mac OS X);
2015-01-21, by wenzelm
updated jdk-8u31;
2015-01-21, by wenzelm
generalized sum_diff_distrib to setsum_subtractf_nat
2015-01-20, by hoelzl
tuned measurability proofs
2015-01-16, by hoelzl
typo in description
2015-01-19, by blanchet
tuned message;
2015-01-19, by wenzelm
always swap panels, which leads to slightly better GUI layout;
2015-01-19, by wenzelm
suppress inactive controls (again);
2015-01-19, by wenzelm
tuned colors;
2015-01-19, by wenzelm
tuned;
2015-01-19, by wenzelm
more symmetric layout of main panel;
2015-01-19, by wenzelm
clarified edge_color;
2015-01-19, by wenzelm
proper tooltips -- override action toolTip which is empty here;
2015-01-19, by wenzelm
no document here;
2015-01-19, by wenzelm
discontinued attempt at alphabetic_order -- selection via regex should be sufficient;
2015-01-18, by wenzelm
suppress some controls that don't work yet;
2015-01-18, by wenzelm
proper selection of nodes via regular expression;
2015-01-18, by wenzelm
obsolete -- full layout takes approx. 100ms;
2015-01-18, by wenzelm
suppress some controls that don't work yet;
2015-01-18, by wenzelm
tuned;
2015-01-18, by wenzelm
misc tuning;
2015-01-18, by wenzelm
proper scrolling wrt. transform;
2015-01-18, by wenzelm
clarified main actions and keyboard focus;
2015-01-18, by wenzelm
tuned signature;
2015-01-18, by wenzelm
retain uniform background, notably wrt. PDF output and tree panel;
2015-01-18, by wenzelm
option graphview_swap_panels;
2015-01-18, by wenzelm
support for tree view on graph nodes;
2015-01-18, by wenzelm
tuned;
2015-01-18, by wenzelm
no censorship of L&F;
2015-01-18, by wenzelm
prefer fractional font metrics, for proper scaling of node size;
2015-01-18, by wenzelm
tuned metrics;
2015-01-18, by wenzelm
tuned window size for the sake of Windows L&F;
2015-01-17, by wenzelm
proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;
2015-01-17, by wenzelm
more compact content for tighter graph layout;
2015-01-17, by wenzelm
more explicit Layout.Info: size and content;
2015-01-17, by wenzelm
clarified Class.pretty_specification: imitate input source;
2015-01-17, by wenzelm
merged
2015-01-16, by boehmes
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
2015-01-16, by boehmes
added simp lemma
2015-01-16, by nipkow
tuned
2015-01-15, by haftmann
separate image for prerequisites of codegen tutorial
2015-01-15, by haftmann
modernized cartouches
2015-01-15, by haftmann
even more pervasive replacement of auxiliary destination
2015-01-15, by haftmann
merged
2015-01-15, by boehmes
more detailed runtime statistics for Z3 proof reconstruction
2015-01-15, by boehmes
merged
2015-01-15, by wenzelm
proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
2015-01-15, by wenzelm
updated to scala-2.11.5;
2015-01-15, by wenzelm
refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;
2015-01-15, by wenzelm
more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-15, by wenzelm
tuned;
2015-01-15, by wenzelm
more type-safe handler interface;
2015-01-14, by wenzelm
clarified build_theories: proper protocol handler;
2015-01-14, by wenzelm
added Promise.cancel;
2015-01-14, by wenzelm
clarified build_theories;
2015-01-14, by wenzelm
added Path.decode in ML, in correspondence to Path.encode in Scala;
2015-01-14, by wenzelm
some support for PIDE batch session;
2015-01-13, by wenzelm
piecewise measurability using restrict_space; cleanup Borel_Space
2015-01-15, by hoelzl
tuned
2015-01-14, by nipkow
indent broken lines of bindings in do blocks
2015-01-14, by Andreas Lochbihler
more line breaks in integral notation
2015-01-14, by Andreas Lochbihler
allow line breaks in integral notation
2015-01-14, by Andreas Lochbihler
allow line breaks in probability syntax
2015-01-14, by Andreas Lochbihler
don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it
2015-01-14, by blanchet
NEWS
2015-01-13, by hoelzl
measurability prover: removed app splitting, replaced by more powerful destruction rules
2015-01-13, by hoelzl
tuned warnings: observe Context_Position.is_visible;
2015-01-11, by wenzelm
removed unused/non-portable with_tmp_fifo;
2015-01-11, by wenzelm
discontinued fifo channel, always use portable socket;
2015-01-11, by wenzelm
tuned -- more Sidekick-friendly layout;
2015-01-11, by wenzelm
do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);
2015-01-11, by wenzelm
more explicit errors;
2015-01-11, by wenzelm
proper latex;
2015-01-10, by wenzelm
tuned -- less redundant;
2015-01-10, by wenzelm
proper Session.save with shutdown, which is relevant to avoid persistent threads;
2015-01-10, by wenzelm
tuned latex;
2015-01-10, by wenzelm
merged
2015-01-10, by wenzelm
always use socket to test performance and stability;
2015-01-10, by wenzelm
explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image;
2015-01-10, by wenzelm
tuned;
2015-01-10, by wenzelm
discontinued worker_trend: prefer constant number of active + reserve threads;
2015-01-10, by wenzelm
tuned;
2015-01-10, by wenzelm
added lemma
2015-01-10, by nipkow
typo
2015-01-10, by haftmann
avoid writing into source
2015-01-10, by haftmann
clarified active_job: take dependencies into account (e.g. future based on promise);
2015-01-09, by wenzelm
tuned;
2015-01-09, by wenzelm
non-strict print_state: display old proof state on failure, e.g. unfinished command;
2015-01-09, by wenzelm
permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;
2015-01-09, by wenzelm
clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish;
2015-01-09, by wenzelm
ignore print process even after fork, to avoid loosing active worker threads;
2015-01-09, by wenzelm
rel_pmf OO: conversion to nat is not necessary
2015-01-09, by hoelzl
merged
2015-01-09, by Andreas Lochbihler
simplify construction for distribution of rel_pmf over op OO
2015-01-09, by Andreas Lochbihler
prefer option for default code printing width
2015-01-09, by haftmann
modernized and more uniform style
2015-01-09, by haftmann
tuned order
2015-01-08, by haftmann
tuned
2015-01-08, by haftmann
avoid technical term "mixin" in user documentation text
2015-01-08, by haftmann
tuned;
2015-01-08, by wenzelm
merged
2015-01-07, by nipkow
updated bibtex
2015-01-07, by nipkow
tuned;
2015-01-07, by wenzelm
misc tuning;
2015-01-07, by wenzelm
made SML/NJ happier
2015-01-07, by blanchet
configurable options;
2015-01-07, by wenzelm
proper level distance according to number of edges, as in old browser;
2015-01-06, by wenzelm
clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;
2015-01-06, by wenzelm
tuned;
2015-01-06, by wenzelm
merged
2015-01-06, by wenzelm
NEWS;
2015-01-06, by wenzelm
rubberband method as in old browser;
2015-01-06, by wenzelm
tuned;
2015-01-06, by wenzelm
tuned signature;
2015-01-06, by wenzelm
proper translate vertex (cf. 4d985afc0565);
2015-01-06, by wenzelm
tuned signature;
2015-01-06, by wenzelm
explict layout graph structure, with dummies and coordinates;
2015-01-06, by wenzelm
tuned;
2015-01-06, by wenzelm
docs
2015-01-06, by blanchet
docs
2015-01-06, by blanchet
docs
2015-01-06, by blanchet
tuning
2015-01-06, by blanchet
formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
2015-01-05, by haftmann
merged
2015-01-05, by wenzelm
clarified visualizer parameters;
2015-01-05, by wenzelm
tuned metrics;
2015-01-05, by wenzelm
proper bounding box including dummies;
2015-01-05, by wenzelm
more direct coordinates for dummy;
2015-01-05, by wenzelm
separate module Metrics;
2015-01-05, by wenzelm
tuned imports;
2015-01-05, by wenzelm
apply layout on change of options;
2015-01-05, by wenzelm
avoid fractional font size;
2015-01-05, by wenzelm
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
2015-01-05, by wenzelm
eliminated print modes: offer new and old graph;
2015-01-05, by wenzelm
docs
2015-01-05, by blanchet
generate [code] only with 'code' plugin enabled
2015-01-05, by blanchet
docs
2015-01-05, by blanchet
added plugins syntax to prim(co)rec
2015-01-05, by blanchet
docs
2015-01-05, by blanchet
tuning
2015-01-05, by blanchet
docs
2015-01-05, by blanchet
documented 'transfer' options to 'prim(co)rec'
2015-01-05, by blanchet
tuning
2015-01-05, by blanchet
Add plugin to generate transfer theorem for primrec and primcorec
2014-12-19, by desharna
use proper context in function
2014-12-19, by desharna
document 'disc_eq_case'
2014-12-19, by desharna
tuning
2015-01-05, by blanchet
generate 'disc_eq_case' for Ctr_Sugars
2014-12-19, by desharna
tuning
2015-01-05, by blanchet
remove duplication in tactic
2014-12-19, by desharna
document 'case_distrib'
2014-12-19, by desharna
tuning
2015-01-05, by blanchet
generate 'case_distrib' for Ctr_Sugars
2014-12-19, by desharna
more metrics, with integer coordinates for layout;
2015-01-05, by wenzelm
tuned;
2015-01-04, by wenzelm
misc tuning;
2015-01-04, by wenzelm
explicit Layout.Point;
2015-01-04, by wenzelm
tuned comments;
2015-01-04, by wenzelm
tuned;
2015-01-04, by wenzelm
clarified static full_graph vs. dynamic visible_graph;
2015-01-04, by wenzelm
tuned signature;
2015-01-04, by wenzelm
tuned -- more iterators;
2015-01-03, by wenzelm
tuned;
2015-01-03, by wenzelm
clarified fit_to_window: floor scale within window bounds;
2015-01-03, by wenzelm
tuned;
2015-01-03, by wenzelm
apply_layout: proper repaint;
2015-01-03, by wenzelm
tuned;
2015-01-03, by wenzelm
tuned;
2015-01-03, by wenzelm
tuned;
2015-01-03, by wenzelm
tuned;
2015-01-03, by wenzelm
tuned signature;
2015-01-03, by wenzelm
tuned menu items;
2015-01-03, by wenzelm
tuned signature;
2015-01-03, by wenzelm
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
2015-01-03, by wenzelm
more uniform support for graph display in ML/Scala;
2015-01-03, by wenzelm
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
2015-01-03, by wenzelm
prefer integer coordinates;
2015-01-03, by wenzelm
clarified bounding box, similar to old graph browser;
2015-01-03, by wenzelm
tuned headers;
2015-01-02, by wenzelm
less excessive event handling;
2015-01-02, by wenzelm
tuned;
2015-01-02, by wenzelm
clarified mouse wheel: conventional scrolling, not scaling;
2015-01-02, by wenzelm
clarified metrics, similar to old graph browser;
2015-01-02, by wenzelm
merged
2015-01-01, by wenzelm
tuned color;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
more dynamic visualizer -- re-use jEdit font info;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
more dynamic visualizer -- re-use Isabelle/jEdit options;
2015-01-01, by wenzelm
more standard GUI layout;
2015-01-01, by wenzelm
tuned;
2015-01-01, by wenzelm
tuned imports;
2015-01-01, by wenzelm
tuned;
2015-01-01, by wenzelm
tuned imports;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
tuned signature;
2015-01-01, by wenzelm
tuned;
2015-01-01, by wenzelm
tuned whitespace;
2015-01-01, by wenzelm
merged
2015-01-01, by boehmes
updated NEWS
2015-01-01, by boehmes
optionally display statistics for Z3 proof reconstruction
2014-12-29, by boehmes
avoid more than one data slot per module
2014-12-29, by boehmes
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
2014-12-29, by boehmes
converse graph according to Graph_Display;
2014-12-31, by wenzelm
eliminated TTY/PG legacy;
2014-12-31, by wenzelm
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
2014-12-31, by wenzelm
tuned;
2014-12-31, by wenzelm
for graph display, prefer graph data structure over list with dependencies;
2014-12-31, by wenzelm
more explict and generic field names
2014-12-31, by wenzelm
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
2014-12-31, by wenzelm
stripped ad-hoc diagnostic facility
2014-12-31, by wenzelm
update map definition in Prog_Prove for new datatype package
2014-12-31, by kleing
explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-30, by wenzelm
clarified source location;
2014-12-30, by wenzelm
added system property isabelle.laf, notably for initial system dialog;
2014-12-30, by wenzelm
NEWS;
2014-12-30, by wenzelm
tuned;
2014-12-29, by wenzelm
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
2014-12-29, by wenzelm
tuned whitespace;
2014-12-29, by wenzelm
more toplevel pretty printing;
2014-12-29, by wenzelm
back to full synchronization (cf. eb3e399f5b9f);
2014-12-28, by wenzelm
proper sequential version;
2014-12-28, by wenzelm
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
2014-12-28, by wenzelm
modernized historic example;
2014-12-28, by wenzelm
more thorough Lazy.is_finished;
2014-12-28, by wenzelm
3 old example lemmas by Amine listed in the top 100 theorems
2014-12-28, by kleing
update_cartouches;
2014-12-27, by wenzelm
memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;
2014-12-27, by wenzelm
typos
2014-12-24, by haftmann
unused;
2014-12-23, by wenzelm
tuned message;
2014-12-23, by wenzelm
explicit message channels for "state", "information";
2014-12-23, by wenzelm
imitate font more carefully: err on smaller size;
2014-12-23, by wenzelm
more accurate selection of sessions;
2014-12-22, by wenzelm
more accurate selection of sessions;
2014-12-22, by wenzelm
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
2014-12-22, by wenzelm
more elementary Multithreading.synchronized;
2014-12-22, by wenzelm
proper Synchronized.var;
2014-12-22, by wenzelm
removed remains from Proof General;
2014-12-22, by wenzelm
obsolete;
2014-12-22, by wenzelm
system option "pretty_margin" is superseded by "thy_output_margin";
2014-12-22, by wenzelm
tuned;
2014-12-22, by wenzelm
proper Synchronized.var;
2014-12-22, by wenzelm
separate module Random;
2014-12-22, by wenzelm
tuned;
2014-12-21, by wenzelm
tuned signature;
2014-12-21, by wenzelm
proper context;
2014-12-21, by wenzelm
afford more heap;
2014-12-21, by wenzelm
increase chances of success;
2014-12-21, by wenzelm
recovered metis proof after 115965966e15 (Odd clash of type variables!?);
2014-12-21, by wenzelm
proper context;
2014-12-21, by wenzelm
proper context for "net" tactics;
2014-12-20, by wenzelm
tuned;
2014-12-20, by wenzelm
afford full test, with slightly improved scheduling order;
2014-12-20, by wenzelm
more generous timeout, to increase chances of at64-poly;
2014-12-19, by wenzelm
updated according to eb3e399f5b9f;
2014-12-19, by wenzelm
just one data slot per program unit;
2014-12-19, by wenzelm
tuned;
2014-12-19, by wenzelm
just one data slot per program unit;
2014-12-19, by wenzelm
more standard configuration options;
2014-12-19, by wenzelm
tuned;
2014-12-19, by wenzelm
just one data slot per program unit;
2014-12-19, by wenzelm
tuned;
2014-12-19, by wenzelm
more frugal Local_Syntax.init -- maintain idents within context;
2014-12-19, by wenzelm
proper exception for internal program failure, not user-error;
2014-12-19, by wenzelm
tuned;
2014-12-19, by wenzelm
suppress irrelevant timing messages (the majority);
2014-12-18, by wenzelm
less ambitious settings -- increase chances of success;
2014-12-18, by wenzelm
peek value without synchronization;
2014-12-18, by wenzelm
avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
2014-12-18, by wenzelm
tuning
2014-12-17, by blanchet
unfortunately, there is no general function space in the measurable spaces
2014-12-17, by hoelzl
correctly apply type substitution before checking for function types
2014-12-15, by blanchet
avoid generating selectors with function types -- this produce arity inconsistencies
2014-12-15, by blanchet
renamed theory file
2014-12-15, by blanchet
merged
2014-12-12, by wenzelm
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
2014-12-12, by wenzelm
tuned;
2014-12-12, by wenzelm
tuned;
2014-12-11, by wenzelm
added Par_List in Scala, in accordance to ML version;
2014-12-11, by wenzelm
tuned;
2014-12-11, by wenzelm
rel_pmf commutes with rel_prod
2014-12-12, by hoelzl
note more facts (always)
2014-12-11, by traytel
conceal typedef more violently
2014-12-11, by traytel
respect order of deads when retrieving bnfs from the database
2014-12-11, by traytel
merged
2014-12-10, by wenzelm
more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
2014-12-10, by wenzelm
more examples;
2014-12-10, by wenzelm
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
2014-12-10, by wenzelm
more markup for improper situations;
2014-12-10, by wenzelm
more explicit markup for improper commands;
2014-12-10, by wenzelm
tuned;
2014-12-10, by wenzelm
imitate command markup and rendering of Isabelle/jEdit in HTML output;
2014-12-09, by wenzelm
tuned signature;
2014-12-09, by wenzelm
more jEdit colors;
2014-12-09, by wenzelm
proper alt_string markup (cf. 2ceb05ee0331);
2014-12-09, by wenzelm
tuned spelling;
2014-12-09, by wenzelm
clarified language context, e.g. relevant for symbol completion within cartouches;
2014-12-09, by wenzelm
tuned signature;
2014-12-09, by wenzelm
proper railsetup;
2014-12-09, by wenzelm
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
2014-12-09, by hoelzl
isatest for Mac OS X Yosemite;
2014-11-22, by wenzelm
tuned spelling;
2014-12-08, by wenzelm
expand ML cartouches to Input.source;
2014-12-08, by wenzelm
merged
2014-12-08, by wenzelm
some special cases for official SML, to treat Isabelle symbols like raw characters;
2014-12-08, by wenzelm
tuned comment;
2014-12-08, by wenzelm
clarified Isabelle/ML strings (refining 72238ea2201c);
2014-12-08, by wenzelm
tuned signature;
2014-12-08, by wenzelm
instance bool and enat as topologies
2014-12-08, by hoelzl
NEWS
2014-12-08, by haftmann
allow multiple inheritance of targets
2014-12-05, by haftmann
tuned module structure
2014-12-04, by haftmann
tuned data structures
2014-12-04, by haftmann
tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
2014-12-04, by haftmann
tuned
2014-12-04, by haftmann
tuned names
2014-12-04, by haftmann
eta-expand all search patterns using schematic place holders
2014-12-04, by haftmann
revert "better" handling of abbreviation from c61fe520602b
2014-12-04, by haftmann
tuned variable names
2014-12-04, by haftmann
turn application-specific Pattern.matches_subterm into an application-private function
2014-12-04, by haftmann
cleaned up mess
2014-12-04, by haftmann
add Poisson and Binomial distribution
2014-12-05, by hoelzl
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
2014-12-05, by hoelzl
proper GUI_Thread context (cf. 7e0d3da6e6d8);
2014-12-04, by wenzelm
more examples;
2014-12-04, by wenzelm
tuned header;
2014-12-04, by wenzelm
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
2014-12-04, by hoelzl
merged
2014-12-03, by wenzelm
node-specific keywords, with session base syntax as default;
2014-12-03, by wenzelm
clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-12-03, by wenzelm
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
2014-12-03, by wenzelm
tuned signature;
2014-12-03, by wenzelm
tuned;
2014-12-03, by wenzelm
clarified token kind;
2014-12-03, by wenzelm
added Untyped.method convenience (for *this* class only);
2014-12-02, by wenzelm
tuned signature -- more explicit types;
2014-12-02, by wenzelm
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
2014-12-02, by wenzelm
node-specific syntax, with base_syntax as default;
2014-12-02, by wenzelm
clarified token marker / syntax for mode vs. buffer;
2014-12-01, by wenzelm
Sidekick syntax is derived from buffer (and its mode), instead of parser name;
2014-12-01, by wenzelm
tuned signature;
2014-12-01, by wenzelm
more merge operations;
2014-12-01, by wenzelm
tuned signature;
2014-12-01, by wenzelm
tuned;
2014-12-01, by wenzelm
prefer E 1.8, now that it's been tried and tested
2014-12-03, by blanchet
more accurate context;
2014-11-30, by wenzelm
update_cartouches;
2014-11-30, by wenzelm
tuned signature;
2014-11-30, by wenzelm
tuned signature;
2014-11-30, by wenzelm
tuned signature -- prefer Input.source;
2014-11-30, by wenzelm
more abstract type Input.source;
2014-11-30, by wenzelm
encode text with control symbols;
2014-11-29, by wenzelm
proper HTML.encode;
2014-11-29, by wenzelm
prefer abbrev for is_unit
2014-11-26, by haftmann
do not conceal inductive predicate names properly, following 4a3747517552
2014-11-26, by haftmann
tuned
2014-11-26, by haftmann
renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-26, by wenzelm
added ML antiquotation @{apply n} or @{apply n(k)};
2014-11-26, by wenzelm
even more exception traces for Document.update, which goes through additional execution wrappers;
2014-11-26, by wenzelm
more informative failure of protocol commands, with exception trace;
2014-11-26, by wenzelm
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
2014-11-26, by wenzelm
tuned proof that pmfs are bnfs
2014-11-25, by hoelzl
projections of pair_pmf (by D. Traytel)
2014-11-25, by hoelzl
merged
2014-11-24, by wenzelm
removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6);
2014-11-24, by wenzelm
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
2014-11-24, by traytel
add congruence solver to measurability prover
2014-11-24, by hoelzl
cleanup measurability prover
2014-11-24, by hoelzl
updated SMT certificates
2014-11-24, by blanchet
added one more CVC4 option that helps Judgment Day (10 theory version)
2014-11-24, by blanchet
tuned whitespace
2014-11-24, by blanchet
keep all 'ctr' theorems
2014-11-24, by blanchet
smoothly handle unit codatatypes in 'primcorec'
2014-11-24, by blanchet
careful with de Bruijn indices
2014-11-24, by blanchet
improved message in 'co' case
2014-11-24, by blanchet
updated NEWS
2014-11-24, by blanchet
no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)
2014-11-24, by blanchet
added Z3 reconstruction rule suggested by F. Maric
2014-11-24, by blanchet
one more CVC4 option that helps
2014-11-24, by blanchet
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
2014-11-24, by blanchet
update CVC4 version docs
2014-11-24, by blanchet
tuned signature;
2014-11-22, by wenzelm
tuned;
2014-11-22, by wenzelm
misc tuning and modernization;
2014-11-22, by wenzelm
misc tuning and modernization;
2014-11-22, by wenzelm
more careful ML source positions, for improved PIDE markup;
2014-11-22, by wenzelm
named_theorems: multiple args;
2014-11-22, by wenzelm
tuned;
2014-11-21, by wenzelm
removed some add-ons from modules that are relevant for the inference kernel;
2014-11-21, by wenzelm
add lemma following a proof suggestion by Joachim Breitner
2014-11-21, by Andreas Lochbihler
add lemma
2014-11-21, by Andreas Lochbihler
register pmf as BNF
2014-11-21, by Andreas Lochbihler
added CVC4 option that helps on JD
2014-11-20, by blanchet
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
2014-11-20, by blanchet
work around bug in CVC4, with boolean arguments to (co)datatypes
2014-11-20, by blanchet
other way of crashing (with CVC4)
2014-11-20, by blanchet
set right logic for CVC4 with (co)datatypes
2014-11-20, by blanchet
removed explicit '--quant-cf' option to CVC4, now that it's the default
2014-11-20, by blanchet
more accurate lemma name
2014-11-19, by traytel
parse CVC4 unsat cores
2014-11-19, by blanchet
tuning
2014-11-19, by blanchet
removed redundant code line
2014-11-19, by blanchet
clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
2014-11-18, by wenzelm
add reindex rules for distr and nn_integral on count_space
2014-11-17, by hoelzl
generalized lemmas and tuned proofs
2014-11-17, by haftmann
generalized lemmas (particularly concerning dvd) as far as appropriate
2014-11-17, by haftmann
formally self-contained gcd type classes
2014-11-17, by haftmann
merged
2014-11-14, by wenzelm
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
2014-11-14, by wenzelm
use \isastyletext directly via 'text' command;
2014-11-14, by wenzelm
proper sequential version (cf. 302104d8366b);
2014-11-14, by wenzelm
documentation stubs about permanent_interpretation
2014-11-14, by haftmann
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
2014-11-14, by hoelzl
merged
2014-11-14, by hoelzl
import general theorems from AFP/Markov_Models
2014-11-13, by hoelzl
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
2014-11-13, by wenzelm
tuning
2014-11-13, by blanchet
merged
2014-11-13, by traytel
do not introduce consts too early unnecessarily
2014-11-13, by traytel
added lemma
2014-11-13, by nipkow
merged
2014-11-12, by wenzelm
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
2014-11-12, by wenzelm
make SML/NJ happy;
2014-11-12, by wenzelm
more careful ML source positions, for improved PIDE markup;
2014-11-12, by wenzelm
NEWS
2014-11-12, by immler
tuned proofs
2014-11-12, by immler
added quickcheck[approximation]
2014-11-12, by immler
quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
2014-11-12, by immler
disjunction and conjunction for forms
2014-11-12, by immler
truncate intermediate results in horner to improve performance of approximate;
2014-11-12, by immler
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
2014-11-12, by immler
cancel real of power of numeral also for equality and strict inequality;
2014-11-12, by immler
simplified computations based on round_up by reducing to round_down;
2014-11-12, by immler
code equation for powr
2014-11-12, by immler
merged
2014-11-11, by wenzelm
more careful ML source positions, for improved PIDE markup;
2014-11-11, by wenzelm
more position information, e.g. relevant for errors in generated ML source;
2014-11-11, by wenzelm
more symbols;
2014-11-11, by wenzelm
tuned whitespace;
2014-11-11, by wenzelm
more markup;
2014-11-11, by wenzelm
simplifie sessions;
2014-11-11, by wenzelm
more Isar proof methods;
2014-11-11, by wenzelm
more Isar proof methods;
2014-11-11, by wenzelm
more Isar proof methods;
2014-11-11, by wenzelm
add forgotten lemma
2014-11-11, by noschinl
added lemma
2014-11-11, by noschinl
make 'corec_transfer' tactic more robust
2014-11-11, by desharna
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
2014-11-11, by desharna
make 'rec_transfer' tactic more robust
2014-11-11, by desharna
add del option to measurable;
2014-11-11, by Andreas Lochbihler
merged
2014-11-11, by wenzelm
proper context for assume_tac (atac remains as fall-back without context);
2014-11-10, by wenzelm
even -> evn because even is now in Main
2014-11-10, by nipkow
dropped redundant transfer rules (now proved and registered by datatype and plugins)
2014-11-10, by traytel
proper context for typedef;
2014-11-09, by wenzelm
proper proof context for typedef;
2014-11-09, by wenzelm
proper context;
2014-11-09, by wenzelm
proper context for match_tac etc.;
2014-11-09, by wenzelm
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-09, by wenzelm
avoid erule and rotated in IMP
2014-11-09, by nipkow
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
2014-11-09, by haftmann
self-contained simp rules for dvd on numerals
2014-11-09, by haftmann
equivalence rules for structures without zero divisors
2014-11-08, by haftmann
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
2014-11-08, by wenzelm
optional proof context for unify operations, for the sake of proper local options;
2014-11-08, by wenzelm
clarified name of Type.unified, to emphasize its connection to the "unify" family;
2014-11-08, by wenzelm
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
tuned spelling;
2014-10-30, by wenzelm
hardwired imitation of copy.shortcut2 default;
2014-10-30, by wenzelm
more simp rules concerning dvd and even/odd
2014-10-30, by haftmann
choose_reduce_nat: re-ordered operands
2014-10-30, by paulson
make SML/NJ more happy;
2014-10-30, by wenzelm
proper syntax categery "name" -- as usual and as documented;
2014-10-30, by wenzelm
disable coercions for NO_MATCH
2014-10-30, by hoelzl
merged
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
merged
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
tuned;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
modernized setup;
2014-10-29, by wenzelm
more standard theory name;
2014-10-29, by wenzelm
more iterators;
2014-10-29, by wenzelm
removed useless lemmas
2014-10-29, by nipkow
tuned layout and proofs
2014-10-29, by nipkow
tuned proofs;
2014-10-28, by wenzelm
increase chances that HOL-Proofs image still works for polyml-5.3.0;
2014-10-28, by wenzelm
tuned signature;
2014-10-28, by wenzelm
proper selectMatch, e.g. relevant for S-click on gutter;
2014-10-28, by wenzelm
find command span in buffer;
2014-10-28, by wenzelm
'notepad' requires proper nesting of begin/end;
2014-10-28, by wenzelm
explicit keyword category for commands that may start a block;
2014-10-28, by wenzelm
updated keywords;
2014-10-28, by wenzelm
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-10-28, by wenzelm
more abstract type;
2014-10-28, by wenzelm
tuned;
2014-10-28, by wenzelm
tuned;
2014-10-28, by wenzelm
updated to jdk-7u72;
2014-10-27, by wenzelm
increase chances that HOL-Proofs image still works for polyml-5.3.0;
2014-10-27, by wenzelm
JRE is sufficient for official release -- javac and jar are only needed for self-build;
2014-10-27, by wenzelm
clarified ISABELLE_JDK_HOME vs. JAVA_HOME;
2014-10-27, by wenzelm
ISABELLE_JAVA_EXT is obsolete;
2014-10-27, by wenzelm
further generalization of natfloor_div_nat
2014-10-27, by hoelzl
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
2014-10-27, by hoelzl
eliminated redundancies;
2014-10-26, by haftmann
more simp rules;
2014-10-25, by haftmann
clarified default;
2014-10-26, by wenzelm
support negative extraLineSpacing;
2014-10-26, by wenzelm
tuned whitespace;
2014-10-25, by wenzelm
made SML/NJ happy;
2014-10-25, by wenzelm
merged;
2014-10-24, by wenzelm
discontinued python from standard system environment;
2014-10-24, by wenzelm
more generous default;
2014-10-24, by wenzelm
even further downshift of theory Parity in the hierarchy
2014-10-23, by haftmann
further downshift of theory Parity in the hierarchy
2014-10-23, by haftmann
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-24, by hoelzl
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
2014-10-24, by hoelzl
repaired long-standing accident
2014-10-23, by haftmann
explicit definition restores HOL Light import after cb9d84d3e7f2
2014-10-23, by haftmann
tuned language and spelling
2014-10-23, by haftmann
slight generalization and unification of simp rules for algebraic procedures
2014-10-23, by haftmann
downshift of theory Parity in the hierarchy
2014-10-23, by haftmann
parity induction over natural numbers
2014-10-23, by haftmann
merged
2014-10-22, by wenzelm
proper line height and text base line, like regular TextAreaPainter.PaintText;
2014-10-22, by wenzelm
tuned imports;
2014-10-22, by wenzelm
merged
2014-10-22, by Andreas Lochbihler
add print translation for probability notation \<P>
2014-10-22, by Andreas Lochbihler
find main command keyword of 'begin';
2014-10-22, by wenzelm
restricted scanning;
2014-10-22, by wenzelm
repaired rail diagram (cf. 8450b944e58a);
2014-10-22, by wenzelm
foldPainter like Windows L&F;
2014-10-21, by wenzelm
merged
2014-10-21, by wenzelm
NEWS;
2014-10-21, by wenzelm
tuned whitespace;
2014-10-21, by wenzelm
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
2014-10-21, by wenzelm
support for proof structure matching;
2014-10-21, by wenzelm
tuned;
2014-10-21, by wenzelm
tuned;
2014-10-21, by wenzelm
support for begin/end matching;
2014-10-21, by wenzelm
proper token kind;
2014-10-21, by wenzelm
added option jedit_structure_limit;
2014-10-21, by wenzelm
some structure matching, based on line token iterators;
2014-10-21, by wenzelm
support for structure matching;
2014-10-21, by wenzelm
tuned rendering;
2014-10-21, by wenzelm
back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;
2014-10-21, by wenzelm
tuned;
2014-10-21, by wenzelm
update_cartouches;
2014-10-21, by wenzelm
clarified tree root;
2014-10-21, by wenzelm
tuned spacing;
2014-10-21, by wenzelm
clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
2014-10-21, by wenzelm
turn even into an abbreviation
2014-10-21, by haftmann
update documentation for 'size_o_map'
2014-10-21, by desharna
rename 'size_o_map' to 'size_gen_o_map'
2014-10-21, by desharna
document 'size_gen'
2014-10-21, by desharna
generate 'size_gen' for datatypes
2014-10-21, by desharna
document 'map_o_corec'
2014-10-21, by desharna
generate 'map_o_corec' for (co)datatypes
2014-10-21, by desharna
move documentation of 'rec_o_map'
2014-10-21, by desharna
move theorem 'rec_o_map'
2014-10-21, by desharna
warn for not fully mutually (co)recursive types
2014-10-21, by desharna
add transfer rule for set_pmf
2014-10-21, by hoelzl
add tendsto_const and tendsto_ident_at as simp and intro rules
2014-10-20, by hoelzl
tuned spacing;
2014-10-20, by wenzelm
avoid odd ligatures;
2014-10-20, by wenzelm
more accurate approximation of AST;
2014-10-20, by wenzelm
tuned exposition of {* ... *};
2014-10-20, by wenzelm
more antiquotations;
2014-10-20, by wenzelm
more antiquotations;
2014-10-20, by wenzelm
register transfer rules from BNF and FP_Sugar
2014-10-20, by kuncar
refactored
2014-10-20, by kuncar
merged
2014-10-20, by wenzelm
back to formal comment (see 23a380cc45f4, 3094b0edd6b5);
2014-10-20, by wenzelm
repared document;
2014-10-20, by wenzelm
merged
2014-10-20, by wenzelm
official support for "tt" style variants, avoid fragile \verb in LaTeX;
2014-10-20, by wenzelm
removed dead code;
2014-10-20, by wenzelm
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
2014-10-20, by wenzelm
tweaked
2014-10-20, by paulson
avoid unsafe simp rules
2014-10-20, by haftmann
more standard declaration for presburger
2014-10-20, by haftmann
augmented and tuned facts on even/odd and division
2014-10-20, by haftmann
prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-10-19, by haftmann
NEWS;
2014-10-19, by wenzelm
omit pointless nodes for proof commands etc.;
2014-10-19, by wenzelm
tuned signature and modules;
2014-10-19, by wenzelm
merged
2014-10-18, by wenzelm
NEWS;
2014-10-18, by wenzelm
more folds;
2014-10-18, by wenzelm
always apply precedingFoldLevels, avoid unclear shortcuts;
2014-10-18, by wenzelm
make double-sure that line context is present, e.g. relevant for last line after visible text;
2014-10-18, by wenzelm
clarified Line_Structure wrt. command span;
2014-10-18, by wenzelm
tuned signature;
2014-10-18, by wenzelm
tuned signature;
2014-10-18, by wenzelm
tuned signature;
2014-10-18, by wenzelm
more explicit Line_Nesting;
2014-10-16, by wenzelm
tuned comments;
2014-10-16, by wenzelm
support line context with depth;
2014-10-16, by wenzelm
proper type comparison (amending cd4439d8799c);
2014-10-16, by wenzelm
tuned;
2014-10-16, by wenzelm
tuned
2014-10-16, by haftmann
standard elimination rule for even
2014-10-16, by haftmann
tuned facts on even and power
2014-10-16, by haftmann
restructured
2014-10-16, by haftmann
even more cleanup
2014-10-16, by haftmann
made SML/NJ happier
2014-10-16, by blanchet
made SML/NJ happier
2014-10-15, by blanchet
tuned whitespace
2014-10-15, by blanchet
buffer_line_context via untyped access;
2014-10-14, by wenzelm
access class hierarchy;
2014-10-14, by wenzelm
legacy cleanup
2014-10-14, by haftmann
more algebraic deductions for facts on even/odd
2014-10-14, by haftmann
more algebraic deductions for facts on even/odd
2014-10-14, by haftmann
purely algebraic characterization of even and odd
2014-10-14, by haftmann
document 'sel_transfer'
2014-10-14, by desharna
generate 'sel_transfer' for (co)datatypes
2014-10-14, by desharna
add 'kind' to 'cr_sugar'
2014-10-14, by desharna
add 'fp_bnf' to 'bnf_sugar'
2014-10-14, by desharna
preserve the structure of 'set_intros' theorem in ML
2014-10-14, by desharna
preserve the structure of 'map_sel' theorem in ML
2014-10-14, by desharna
preserve the structure of 'set_sel' theorem in ML
2014-10-14, by desharna
Fixed bug in waldmeister skolemization
2014-10-14, by steckerm
tuned signature;
2014-10-14, by wenzelm
tuned signature;
2014-10-13, by wenzelm
merged
2014-10-13, by wenzelm
tuned signature;
2014-10-13, by wenzelm
tuned signature;
2014-10-13, by wenzelm
obsolete;
2014-10-13, by wenzelm
module Interpretation is superseded by Plugin;
2014-10-13, by wenzelm
module Interpretation is superseded by Plugin;
2014-10-13, by wenzelm
module Interpretation is superseded by Plugin;
2014-10-13, by wenzelm
clarified load order;
2014-10-13, by wenzelm
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-10-13, by wenzelm
support for indirections (defined entries), e.g. relevant for quickcheck and its sub-plugins;
2014-10-13, by wenzelm
support for named plugins for definitional packages;
2014-10-13, by wenzelm
relaxed class constraints for exp
2014-10-13, by immler
tuned
2014-10-13, by nipkow
special treatment of extensionality in minimizer
2014-10-12, by blanchet
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
2014-10-12, by blanchet
made SML/NJ happier
2014-10-12, by blanchet
leftover from 3ccafeb9a1d1
2014-10-12, by haftmann
some more facts on divisibility
2014-10-12, by haftmann
generalized and consolidated some theorems concerning divisibility
2014-10-12, by haftmann
eliminiated clone
2014-10-12, by haftmann
more facts about abstract divisibility
2014-10-12, by haftmann
specialized specification: avoid trivial instances
2014-10-10, by haftmann
more foundational definition for predicate even
2014-10-09, by haftmann
New example Bubblesort
2014-10-10, by nipkow
formally completeted set of experimental static evaluation functions
2014-10-09, by haftmann
merged
2014-10-09, by wenzelm
afford slightly bigger JVM stack (see also f7ba30a816b9);
2014-10-09, by wenzelm
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
2014-10-09, by wenzelm
prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;
2014-10-09, by wenzelm
proper @{cite} with bibtex entry (unchecked comment);
2014-10-09, by wenzelm
fix document generation in Code_Test
2014-10-09, by hoelzl
merged
2014-10-08, by wenzelm
eliminated some exotic combinators;
2014-10-08, by wenzelm
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-10-08, by wenzelm
tuned;
2014-10-08, by wenzelm
tuned;
2014-10-08, by wenzelm
clarified messages depending on options;
2014-10-08, by wenzelm
simplified "sos" method;
2014-10-08, by wenzelm
tuned signature;
2014-10-08, by wenzelm
tuned spelling;
2014-10-08, by wenzelm
add Linear Temporal Logic on Streams
2014-10-08, by hoelzl
move Code_Test to HOL/Library;
2014-10-08, by Andreas Lochbihler
proper bibliography;
2014-10-08, by wenzelm
more antiquotations;
2014-10-07, by wenzelm
more bibtex entries;
2014-10-07, by wenzelm
more antiquotations;
2014-10-07, by wenzelm
tuned whitespace;
2014-10-07, by wenzelm
more antiquotations;
2014-10-07, by wenzelm
clarified whitespace;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
merged
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
more symbols;
2014-10-07, by wenzelm
more cartouches;
2014-10-07, by wenzelm
added update_cartouches tool;
2014-10-07, by wenzelm
removed pointless regexp flags;
2014-10-07, by wenzelm
fix document generation for HOL-Probability
2014-10-07, by hoelzl
move Stream theory from Datatype_Examples to Library
2014-10-07, by hoelzl
add Giry monad
2014-10-07, by hoelzl
tuned
2014-10-06, by nipkow
improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;
2014-10-06, by wenzelm
merged
2014-10-06, by nipkow
tuned spaces
2014-10-06, by nipkow
avoid creating needless skolemization steps for SPASS
2014-10-06, by blanchet
get rid of 'individual' type in DFG proofs
2014-10-06, by blanchet
slightly nicer names
2014-10-06, by blanchet
strengthened 'moura' method
2014-10-06, by blanchet
improved unskolemization of SPASS problems
2014-10-06, by blanchet
more total parser;
2014-10-06, by wenzelm
more defensive error handling -- token marker must not crash;
2014-10-06, by wenzelm
merged
2014-10-06, by wenzelm
documentation of @{cite} and cite_macro;
2014-10-06, by wenzelm
completion for bibtex entries;
2014-10-06, by wenzelm
more accurate item name, depending on kind;
2014-10-06, by wenzelm
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
2014-10-06, by wenzelm
tuned signature;
2014-10-06, by wenzelm
add measure space for (coinductive) streams
2014-10-06, by hoelzl
add type for probability mass functions, i.e. discrete probability distribution
2014-10-06, by hoelzl
refactor 'map_sel_thms' and 'set_sel_thms'
2014-10-06, by desharna
rename 'xtor_rel_thms' to 'xtor_rels'
2014-10-06, by desharna
rename 'xtor_set_thmss' to 'xtor_setss'
2014-10-06, by desharna
rename 'xtor_map_thms' to 'xtor_maps'
2014-10-06, by desharna
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
2014-10-06, by desharna
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
2014-10-06, by desharna
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
2014-10-06, by desharna
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
2014-10-06, by desharna
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
2014-10-06, by desharna
add 'set_inducts' to 'fp_sugar'
2014-10-06, by desharna
add 'common_set_inducts' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_co_inducts' to 'fp_sugar'
2014-10-06, by desharna
add 'common_rel_co_induct' to 'fp_sugar'
2014-10-06, by desharna
add 'co_rec_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'co_rec_disc_iffs' to 'fp_sugar'
2014-10-06, by desharna
add 'disc_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'case_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'ctr_transfers' to 'fp_sugar'
2014-10-06, by desharna
add 'set_cases' to 'fp_sugar'
2014-10-06, by desharna
add 'set_intros' to 'fp_sugar'
2014-10-06, by desharna
add 'set_sels' to 'fp_sugar'
2014-10-06, by desharna
add 'set_thms' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_cases' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_intros' to 'fp_sugar'
2014-10-06, by desharna
add 'rel_sels' to 'fp_sugar'
2014-10-06, by desharna
add 'map_sels' to 'fp_sugar'
2014-10-06, by desharna
add 'map_disc_iffs' to 'fp_sugar'
2014-10-06, by desharna
code preprocessor tracing also for function transformers
2014-10-05, by haftmann
basic support for fully static evaluator generation without dynamic compiler invocation
2014-10-05, by haftmann
split dynamic from static context
2014-10-05, by haftmann
more refs;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
prefer @{cite} antiquotation;
2014-10-05, by wenzelm
NEWS;
2014-10-05, by wenzelm
more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
clarified modules;
2014-10-05, by wenzelm
citation tooltip/hyperlink based on open buffers with .bib files;
2014-10-05, by wenzelm
bibtex support in ML: document antiquotation @{cite} with markup;
2014-10-05, by wenzelm
maintain Document_Model.bibtex_entries;
2014-10-05, by wenzelm
more advanced NEWS tree structure and folding;
2014-10-05, by wenzelm
merged;
2014-10-04, by wenzelm
NEWS;
2014-10-04, by wenzelm
tuned output;
2014-10-04, by wenzelm
proper treatment of @comment (amending 402a8e8107a7);
2014-10-04, by wenzelm
mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);
2014-10-04, by wenzelm
more total chunk_line: recovery via ignored_line;
2014-10-04, by wenzelm
more explicit comments;
2014-10-04, by wenzelm
clarified nesting of delimiters;
2014-10-04, by wenzelm
fields are case-insensitive;
2014-10-04, by wenzelm
clarified nesting of delimiters;
2014-10-04, by wenzelm
more explicit chunk name;
2014-10-04, by wenzelm
clarified Chunk -- avoid ooddities;
2014-10-04, by wenzelm
support for bibtex token markup;
2014-10-04, by wenzelm
more explicit item kind;
2014-10-03, by wenzelm
strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;
2014-10-03, by wenzelm
SideKick parser for bibtex entries;
2014-10-03, by wenzelm
more buffer.isEditable checks;
2014-10-03, by wenzelm
context menu for bibtex entries;
2014-10-03, by wenzelm
some support for bibtex files;
2014-10-02, by wenzelm
tuned
2014-10-03, by nipkow
tuned
2014-10-03, by nipkow
accomplish potentially case-insenstive file systems for Scala
2014-10-02, by haftmann
tuned
2014-10-02, by nipkow
merge
2014-10-02, by blanchet
more precise lemma insertion
2014-10-02, by blanchet
insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem
2014-10-02, by blanchet
avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition
2014-10-02, by blanchet
eliminate duplicate hypotheses (which can arise due to (un)clausification)
2014-10-02, by blanchet
formal lcm definition for polynomials
2014-10-02, by haftmann
moved lemmas out of Int.thy which have nothing to do with int
2014-10-02, by haftmann
redundant: dropped
2014-10-02, by haftmann
tuned Heap_Monad.successE
2014-10-02, by haftmann
documentation
2014-10-02, by blanchet
fixed a few mistakes in the documentation
2014-10-02, by blanchet
tuning
2014-10-02, by blanchet
'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3
2014-10-02, by blanchet
actually finish after closing, e.g. relevant for consecutive (**)(**);
2014-10-01, by wenzelm
tuned
2014-09-30, by nipkow
tuned;
2014-09-30, by wenzelm
tuned
2014-09-30, by nipkow
don't call 'hd' on a possibly empty list
2014-09-30, by blanchet
proper types for applied variables, for typed formats (TFF0, DFG)
2014-09-30, by blanchet
don't affect other subgoals with 'auto' in one-liner proofs
2014-09-30, by blanchet
tuned output in case of one-liner failure
2014-09-30, by blanchet
updated docs with two provers: veriT and Zipperposition
2014-09-30, by blanchet
give more facts to veriT -- it seems to be able to cope with them
2014-09-30, by blanchet
use native encoding with Vampire -- modern versions handle types better than the old ones
2014-09-30, by blanchet
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
2014-09-30, by blanchet
correct inlining in veriT's subproofs.
2014-09-30, by fleury
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
2014-09-30, by blanchet
tuning
2014-09-30, by blanchet
tuning
2014-09-30, by blanchet
keep rules with no premises in Isar proofs from veriT
2014-09-30, by blanchet
correct indexing in the presence of lambda-lifting
2014-09-30, by blanchet
merged
2014-09-29, by nipkow
tuned
2014-09-29, by nipkow
merge
2014-09-29, by blanchet
support hypotheses with schematics in Isar proofs
2014-09-29, by blanchet
tuned
2014-09-29, by nipkow
simplified and repaired veriT index handling code
2014-09-29, by blanchet
made 'moura' tactic more powerful
2014-09-29, by blanchet
fixed wrong optimization (wrong because it may affect the sequent's conclusion)
2014-09-29, by blanchet
merge
2014-09-29, by blanchet
added option to get cleaner SPASS proofs
2014-09-29, by blanchet
parse back type of SPASS proof variables
2014-09-29, by blanchet
make sure no '__' suffixes make it until Isar proof
2014-09-29, by blanchet
rename skolem symbols in the negative case as well
2014-09-29, by blanchet
reintroduced 'rel_cases' in docs
2014-09-29, by blanchet
added options to Mirabelle
2014-09-29, by blanchet
tuning
2014-09-29, by blanchet
faster machine for slow/bulky polyml-5.3.0 tests (notably HOL-Proofs);
2014-09-29, by wenzelm
pro-forma support for polyml-5.5.3 (presently SVN 1960);
2014-09-29, by wenzelm
corrected white-space accident
2014-09-29, by haftmann
tuned
2014-09-28, by haftmann
moved to HOL and generalized
2014-09-28, by haftmann
merged
2014-09-26, by wenzelm
proper range for Antiq tokens;
2014-09-26, by wenzelm
support for sub-expression markup;
2014-09-26, by wenzelm
tuned message;
2014-09-26, by wenzelm
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar move theorems
2014-09-26, by desharna
refactor fp_sugar with empty substructures
2014-09-26, by desharna
add attribute 'case_names' to 'set_case'
2014-09-26, by desharna
make 'case_transfer' tactic more robust
2014-09-26, by desharna
more correct precedence of do-notation
2014-09-25, by haftmann
merged
2014-09-25, by wenzelm
save image as PNG or PDF;
2014-09-25, by wenzelm
support for PNG output;
2014-09-25, by wenzelm
more isatests (on lxbroy4);
2014-09-25, by wenzelm
document 'corec_transfer'
2014-09-25, by desharna
generate 'corec_transfer' for codatatypes
2014-09-25, by desharna
document 'rec_transfer'
2014-09-25, by desharna
generate 'rec_transfer' for datatypes
2014-09-25, by desharna
generate 'dtor_corec_transfer' for codatatypes
2014-09-25, by desharna
generate 'ctor_rec_transfer' for datatypes
2014-09-25, by desharna
goal generation for xtor_co_rec_transfer
2014-09-01, by traytel
commented out some tests that require external tools (e.g. ghc)
2014-09-25, by blanchet
added useful options to CVC4
2014-09-25, by blanchet
subscribe for isatest
2014-09-25, by traytel
even more deads go to the end (continuation of e3a01b73579f)
2014-09-25, by traytel
added function size1
2014-09-25, by nipkow
added lemmas
2014-09-24, by haftmann
tuned
2014-09-24, by haftmann
avoid type variable name clash
2014-09-24, by blanchet
tuning
2014-09-24, by blanchet
made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
2014-09-24, by blanchet
improved 'bnf' parser
2014-09-24, by blanchet
updated SMT certificates
2014-09-24, by blanchet
allow homogeneous nesting for SMT (co)datatypes
2014-09-24, by blanchet
interleave (co)datatypes in the right order w.r.t. dependencies
2014-09-24, by blanchet
rule out nested (co)recursion for SMT (co)datatypes
2014-09-24, by blanchet
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
2014-09-24, by blanchet
tuning
2014-09-24, by blanchet
simpler proof
2014-09-24, by blanchet
added nice standard syntax
2014-09-24, by nipkow
clarified timeout for isatest;
2014-09-22, by wenzelm
merged
2014-09-22, by wenzelm
discontinued old "xnum" token category;
2014-09-22, by wenzelm
added csdp-6.x for proof method (sos csdp);
2014-09-22, by wenzelm
examples for local CSDP executable;
2014-09-22, by wenzelm
clarified SOS tool setup vs. examples;
2014-09-22, by wenzelm
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
2014-09-22, by desharna
merged
2014-09-22, by wenzelm
clarified ISABELLE_POLYML;
2014-09-22, by wenzelm
drop workaround addressed by d0d3c30806b4
2014-09-22, by Andreas Lochbihler
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
2014-09-21, by wenzelm
more standard Isabelle/ML operations;
2014-09-21, by wenzelm
tuned;
2014-09-21, by wenzelm
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-21, by haftmann
corrected slip in documentation
2014-09-21, by haftmann
Removed double space
2014-09-20, by steckerm
Changed proof method to auto for custom Waldmeister lemma
2014-09-20, by steckerm
Minor fixes in ATP_Waldmeister
2014-09-20, by steckerm
Made encoded type for apply less restrictive
2014-09-20, by steckerm
Updated fix_name function
2014-09-20, by steckerm
Added support for partial function application
2014-09-20, by steckerm
Improved equality handling in skolemization
2014-09-20, by steckerm
Re-added hypothesis argument to problem generation
2014-09-20, by steckerm
always annotate potentially polymorphic Haskell numerals
2014-09-18, by haftmann
tuned
2014-09-18, by haftmann
simplified and tuned using signed_string_of_int
2014-09-18, by haftmann
tuned data structure
2014-09-18, by haftmann
tuning
2014-09-19, by blanchet
documented limitations
2014-09-19, by blanchet
more honest 'primcorec' -- don't parse a theorem name that is then ignored
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
added a few tests for 'old_datatype'
2014-09-19, by blanchet
reintroduced old setup for size of basic types
2014-09-19, by blanchet
keep obsolete interpretations in Main, to avoid merge trouble
2014-09-19, by blanchet
made new 'primrec' bootstrapping-capable
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
tuning
2014-09-19, by blanchet
typo
2014-09-19, by traytel
regression tests for n2m
2014-09-19, by traytel
merged
2014-09-19, by Andreas Lochbihler
add lemma
2014-09-18, by Andreas Lochbihler
tuned imports
2014-09-18, by blanchet
removed debugging junk
2014-09-18, by blanchet
help AFP entry 'Free-Groups' to compile
2014-09-18, by blanchet
reintroduced an instantiation of 'size' for 'numerals'
2014-09-18, by blanchet
use selector
2014-09-18, by blanchet
moved old 'size' generator together with 'old_datatype'
2014-09-18, by blanchet
moved datatype realizer to 'old_datatype' and colleagues
2014-09-18, by blanchet
careful with op = in n2m (actually by Dmitriy Traytel)
2014-09-18, by blanchet
fixed attribute name in docs (thanks to Andreas Lochbihler)
2014-09-18, by blanchet
updated NEWS
2014-09-18, by blanchet
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
2014-09-18, by blanchet
increased 'HOL-Proofs' timeout
2014-09-18, by blanchet
made 'mk_pointfree' work again in local theories
2014-09-18, by blanchet
fixed authorship
2014-09-18, by blanchet
product over monoids for lists
2014-09-18, by haftmann
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-09-18, by blanchet
more meaningful record tests
2014-09-18, by blanchet
updated SMT certificates
2014-09-18, by blanchet
tuning
2014-09-17, by blanchet
take out selectors for records -- for derived records, these don't quite have the right type
2014-09-17, by blanchet
register Isabelle selectors as SMT selectors when possible
2014-09-17, by blanchet
added codatatype support for CVC4
2014-09-17, by blanchet
added interface for CVC4 extensions
2014-09-17, by blanchet
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
2014-09-17, by blanchet
tweaked compatibility layer
2014-09-17, by blanchet
avoid clash with Quickcheck's generated 'random_xxx' function
2014-09-17, by blanchet
added missing 'restore' in 'transfer' plugin
2014-09-17, by blanchet
syntactic check to determine when to prove 'nested_size_o_map'
2014-09-17, by blanchet
support (finite values of) codatatypes in Quickcheck
2014-09-17, by blanchet
tuned fact visibility
2014-09-16, by blanchet
register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-16, by blanchet
took out 'old_datatype' examples -- those just cause timeouts in Isatests
2014-09-16, by blanchet
added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-16, by blanchet
added lemma
2014-09-16, by nipkow
add target language evaluators for the value command;
2014-09-16, by Andreas Lochbihler
tuning
2014-09-15, by blanchet
refactoring
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
set 'mono' attribute on 'rel_mono'
2014-09-15, by blanchet
'code' is needed for extraction datatype
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
removed accidental '@{print}'
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
more hints on how to port 'size'
2014-09-15, by blanchet
tuned definition of 'size' function to get nicer properties
2014-09-15, by blanchet
tuning
2014-09-15, by blanchet
document size difference
2014-09-15, by blanchet
generate 'code' attribute only if 'code' plugin is enabled
2014-09-15, by blanchet
disable datatype 'plugins' for internal types
2014-09-14, by blanchet
ported Imperative HOL to new datatypes
2014-09-13, by blanchet
imported patch phantoms
2014-09-13, by blanchet
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
2014-09-12, by blanchet
new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead
2014-09-12, by blanchet
run larger nominal examples only 'ISABELLE_FULL_TEST'
2014-09-12, by blanchet
refactor repeated terms in a single variable
2014-09-12, by desharna
make 'ctr_transfer' tactic more robust
2014-09-12, by desharna
make 'rel_sel' and 'map_sel' tactics more robust
2014-09-12, by desharna
Changing the way the dependencies are managed.
2014-09-12, by fleury
correction in the thf0 parser ("(=)" found in a Satallax proof).
2014-09-12, by fleury
merge
2014-09-12, by blanchet
fixed spellings
2014-09-12, by blanchet
NEWS
2014-09-12, by haftmann
abstract product over monoid for lists
2014-09-11, by haftmann
use proto_base_sort uniformly
2014-09-11, by haftmann
fixed some spelling mistakes
2014-09-11, by blanchet
tuned comment
2014-09-11, by blanchet
more porting to new datatypes
2014-09-11, by blanchet
tuning terminology
2014-09-11, by blanchet
compile
2014-09-11, by blanchet
renamed example theory for consistency
2014-09-11, by blanchet
updated ROOT
2014-09-11, by blanchet
tuned documentation
2014-09-11, by blanchet
updated news
2014-09-11, by blanchet
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
2014-09-11, by blanchet
move datatype benchmarks
2014-09-11, by blanchet
use new datatypes for benchmarks
2014-09-11, by blanchet
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-11, by blanchet
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-11, by blanchet
tuning
2014-09-11, by blanchet
fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
2014-09-11, by blanchet
tuning
2014-09-11, by blanchet
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
2014-09-11, by blanchet
speed up old Nominal by killing type variables
2014-09-11, by blanchet
took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
2014-09-11, by blanchet
more docs
2014-09-11, by blanchet
new deads go to the end
2014-09-11, by traytel
comment
2014-09-11, by blanchet
more material on lists
2014-09-10, by haftmann
explicit check phase to guide type inference of class expression towards one single type variable
2014-09-10, by haftmann
tuned
2014-09-10, by haftmann
dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
2014-09-10, by haftmann
tuning
2014-09-09, by blanchet
proper checks -- the calls data structure may contain spurious entries
2014-09-09, by blanchet
avoid exception
2014-09-09, by blanchet
avoid internal fact
2014-09-09, by blanchet
restored old case names
2014-09-09, by blanchet
compile
2014-09-09, by blanchet
avoid duplicate case names
2014-09-09, by blanchet
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
2014-09-09, by blanchet
preserve case names in '(co)induct' theorems generated by prim(co)rec'
2014-09-09, by blanchet
hide DEADID/ID theorems
2014-09-09, by blanchet
tuning
2014-09-09, by blanchet
more canonical (and correct) local theory threading
2014-09-09, by blanchet
removed 'datatype_compat's that are no longer needed
2014-09-09, by blanchet
documented extraction plugin
2014-09-09, by blanchet
made realizer more robust in the face of nesting through functions
2014-09-09, by blanchet
removed debugging junk
2014-09-09, by blanchet
renamed ML file and module
2014-09-09, by blanchet
made datatype realizer plugin work for new-style datatypes with no nesting
2014-09-09, by blanchet
ported HOL-Proofs-Lambda to new datatypes
2014-09-09, by blanchet
ported HOL-Proofs-Extraction to new datatypes
2014-09-09, by blanchet
made SML/NJ happier
2014-09-09, by blanchet
more porting to new datatypes
2014-09-09, by blanchet
tuned IArray code generator w.r.t. map rel set
2014-09-09, by blanchet
ported Nitpick_Examples to new datatypes
2014-09-09, by blanchet
set 'fundef_cong' attribute also for (co)datatypes with no live type variables
2014-09-09, by blanchet
ported IArray to new datatypes
2014-09-09, by blanchet
prevent infinite loop when type variables are of a non-'type' sort
2014-09-09, by blanchet
tuned code
2014-09-09, by blanchet
ported MicroJava to new datatypes
2014-09-09, by blanchet
rename_tac'd scrips
2014-09-09, by blanchet
ported Unix to new datatypes
2014-09-09, by blanchet
ported Isar_Examples to new datatypes
2014-09-09, by blanchet
ported Decision_Procs to new datatypes
2014-09-09, by blanchet
ported Induct to new datatypes
2014-09-09, by blanchet
half-ported Imperative HOL to new datatypes
2014-09-09, by blanchet
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-09, by blanchet
tuned messages
2014-09-09, by blanchet
rename_tac'd scripts
2014-09-09, by blanchet
reverted 83a8570b44bc, which was a misunderstanding
2014-09-09, by blanchet
rename_tac'd script
2014-09-09, by blanchet
ported Bali to new datatypes
2014-09-09, by blanchet
rename_tac'd scripts
2014-09-09, by blanchet
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-09-09, by blanchet
merged
2014-09-09, by nipkow
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-09-09, by nipkow
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
2014-09-09, by steckerm
more docs
2014-09-08, by blanchet
more documentation
2014-09-08, by blanchet
made 'lifting' plugin more robust
2014-09-08, by blanchet
tuned command descriptions
2014-09-08, by blanchet
generate better internal names, with name of the target type in it
2014-09-08, by blanchet
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
2014-09-08, by blanchet
added flag to 'typedef' to allow concealed definitions
2014-09-08, by blanchet
ported old Nominal to use new datatypes
2014-09-08, by blanchet
made tactic even more robust w.r.t. dead variables
2014-09-08, by traytel
made N2M work with sort constraints (cf. TODO)
2014-09-08, by blanchet
compile
2014-09-08, by blanchet
honour sorts in N2M
2014-09-08, by blanchet
proper sort constraints in map and rel theorems
2014-09-08, by blanchet
made new countable tactic work with sorts other than 'type'
2014-09-08, by blanchet
adapted examples to latest changes
2014-09-08, by blanchet
made code work also in the presence of deads
2014-09-08, by blanchet
export right sorts
2014-09-08, by blanchet
test sorts
2014-09-08, by blanchet
use right sort constraints
2014-09-08, by blanchet
never include hidden names -- these cannot be referenced afterward
2014-09-08, by blanchet
use compatibility layer
2014-09-08, by blanchet
made SML/NJ happire
2014-09-08, by blanchet
export useful functions for users of (co)recursors
2014-09-08, by blanchet
improved caching
2014-09-08, by blanchet
compile
2014-09-08, by blanchet
wildcards in plugins
2014-09-08, by blanchet
improved 'datatype_compat' further for recursion through functions
2014-09-08, by blanchet
no type-based lookup -- these fail in the general, ambiguous case
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
more examples/tests
2014-09-08, by blanchet
tuned docs
2014-09-08, by blanchet
properly note theorems for split recursors
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
updated docs
2014-09-08, by blanchet
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
export one more ML function
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
more compatibility documentation
2014-09-08, by blanchet
refactored MaSh files to avoid regenerating exports on each eval
2014-09-08, by blanchet
added missing 'transpose'
2014-09-08, by blanchet
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
2014-09-08, by blanchet
made tactic more robust w.r.t. dead variables
2014-09-08, by traytel
restrictive options for class dependencies
2014-09-07, by haftmann
separated class_deps command into separate file
2014-09-07, by haftmann
Added translation for lambda expressions in terms.
2014-09-07, by steckerm
explicit theory with additional, less commonly used list operations
2014-09-07, by haftmann
generalized
2014-09-07, by haftmann
theory about sum and product on function bodies
2014-09-06, by haftmann
theory about lexicographic ordering on functions
2014-09-06, by haftmann
added various facts
2014-09-06, by haftmann
Generalised card_length_listsum to all m
2014-09-05, by paulson
added lemma
2014-09-05, by nipkow
updated docs
2014-09-05, by blanchet
pretend code generation is a ctr_sugar plugin
2014-09-05, by blanchet
updated docs
2014-09-05, by blanchet
added 'plugins' option to control which hooks are enabled
2014-09-05, by blanchet
introduced mechanism to filter interpretations
2014-09-05, by blanchet
fixed infinite loops in 'register' functions + more uniform API
2014-09-05, by blanchet
named interpretations
2014-09-05, by blanchet
centralized and cleaned up naming handling
2014-09-05, by blanchet
cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-09-04, by hoelzl
tuned Nitpick and Refute examples, which are too slow on some testing machines
2014-09-04, by blanchet
tweaked setup for datatype realizer
2014-09-04, by blanchet
renamed internal constant
2014-09-04, by blanchet
moved code around
2014-09-04, by blanchet
tuned size function generation
2014-09-04, by blanchet
tuning
2014-09-04, by blanchet
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-09-03, by blanchet
tuned ctr_sugar database handling
2014-09-03, by blanchet
tuned BNF database handling
2014-09-03, by blanchet
intelligible errors instead of tactic failures
2014-09-03, by blanchet
reenabled yet another example
2014-09-03, by blanchet
made new tactic even more robust
2014-09-03, by blanchet
reenabled more examples
2014-09-03, by blanchet
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
2014-09-03, by blanchet
reintroduced more examples
2014-09-03, by blanchet
improved tactic further
2014-09-03, by blanchet
reenabled example
2014-09-03, by blanchet
improved new countability tactic
2014-09-03, by blanchet
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
2014-09-03, by blanchet
more robust exception handling
2014-09-03, by blanchet
added tests for new 'countable_datatype' proof method
2014-09-03, by blanchet
lessen the burden on the caller: sort where necessary in n2m
2014-09-03, by traytel
added compatibility function
2014-09-03, by blanchet
added countable tactic for new-style datatypes
2014-09-03, by blanchet
tuning
2014-09-03, by blanchet
registered 'typerep' as countable again
2014-09-03, by blanchet
moved old datatype material around
2014-09-03, by blanchet
removed vacuous theorem references
2014-09-03, by blanchet
commented out failing tactic (now that 'typerep' is defined using the new package
2014-09-03, by blanchet
tuned imports
2014-09-03, by blanchet
use 'datatype_new'
2014-09-03, by blanchet
use 'datatype_new' in 'Main'
2014-09-03, by blanchet
take out 'x = C' of the simplifier for unit types
2014-09-03, by blanchet
giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
2014-09-03, by blanchet
ported 'Statespace' to support new datatypes as well
2014-09-03, by blanchet
use 'datatype_new' in Quickcheck examples
2014-09-03, by blanchet
more compatibility functions
2014-09-03, by blanchet
codatatypes are not datatypes
2014-09-03, by blanchet
ported Quickcheck to support new datatypes better
2014-09-03, by blanchet
removed more slow Refute tests
2014-09-02, by blanchet
tuned Refute example
2014-09-02, by blanchet
Some work on the new waldmeister integration
2014-09-02, by steckerm
merged
2014-09-02, by boehmes
replay Z3 rewrite steps that lift if-then-else expressions
2014-09-02, by boehmes
test discriminators/selectors in BNF regression suite
2014-09-02, by traytel
merge
2014-09-02, by blanchet
made SML/NJ happier
2014-09-02, by blanchet
tuning
2014-09-02, by blanchet
silenced nonexhaustive primrec warnings
2014-09-02, by traytel
more convenient printing of real numbers after evaluation
2014-09-02, by haftmann
avoid more 'bad background theory' issues
2014-09-01, by blanchet
ported TFL to mixture of old and new datatypes
2014-09-01, by blanchet
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
2014-09-01, by blanchet
ported to use new-style datatypes
2014-09-01, by blanchet
ported Refute to use new datatypes when possible
2014-09-01, by blanchet
renamed BNF theories
2014-09-01, by blanchet
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
2014-09-01, by blanchet
added primrec compatibility function
2014-09-01, by blanchet
more work on compatibility interfaces
2014-09-01, by blanchet
added compatibility examples/tests
2014-09-01, by blanchet
implemented compatibility definition of datatype
2014-09-01, by blanchet
implemented compatibility interpretation
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
tuning
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
more compatibility between old- and new-style datatypes
2014-09-01, by blanchet
added theory-based getters for convenience
2014-09-01, by blanchet
made transfer functions slightly more general
2014-09-01, by blanchet
tuned signatures
2014-09-01, by blanchet
tuning
2014-09-01, by blanchet
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01, by blanchet
tuned structure inclusion
2014-09-01, by blanchet
took out legacy material from 'HOL/Library/Library.thy'
2014-09-01, by blanchet
removed commented out parts
2014-09-01, by blanchet
tuned whitespace
2014-09-01, by blanchet
document 'set_transfer'
2014-09-01, by desharna
generate 'set_transfer' for BNFs
2014-09-01, by desharna
document 'rel_transfer'
2014-09-01, by desharna
generate 'rel_transfer' for BNFs
2014-09-01, by desharna
document 'map_transfer'
2014-09-01, by desharna
note 'map_transfer' more often
2014-09-01, by desharna
separated listsum material
2014-08-31, by haftmann
restored generic value slot, retaining default behaviour and separate approximate command
2014-08-31, by haftmann
convenient printing of (- 1 :: integer) after code evaluation
2014-08-31, by haftmann
inlined unused definition
2014-08-30, by haftmann
add simp rules for divisions of numerals in floor and ceiling.
2014-08-29, by hoelzl
document 'disc_transfer'
2014-08-29, by desharna
generate 'disc_transfer' for (co)datatypes
2014-08-29, by desharna
document 'case_transfer'
2014-08-29, by desharna
generate 'case_transfer' for (co)datatypes
2014-08-29, by desharna
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
2014-08-28, by blanchet
reworked unskolemization for SPASS
2014-08-28, by blanchet
clarified docs
2014-08-28, by blanchet
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
2014-08-28, by blanchet
prefer '0.2 ms' to '249 \<mu>s'
2014-08-28, by blanchet
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
2014-08-28, by blanchet
fixed second computations
2014-08-28, by blanchet
merged minimize and auto_minimize
2014-08-28, by blanchet
pass options to remote Vampire
2014-08-28, by blanchet
removed show stuttering
2014-08-28, by blanchet
generate 'thesis' variable in Sledgehammer Isar proofs
2014-08-28, by blanchet
show microseconds as well (useful when playing with Isar proofs)
2014-08-28, by blanchet
tuned message
2014-08-28, by blanchet
made trace more informative when minimization is enabled
2014-08-28, by blanchet
took out one more occurrence of 'PolyML.makestring'
2014-08-28, by blanchet
try 'skolem' method first for Z3
2014-08-28, by blanchet
tuned tracing output (indirectly)
2014-08-28, by blanchet
going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
2014-08-28, by blanchet
moved skolem method
2014-08-28, by blanchet
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-28, by blanchet
tuned method description
2014-08-28, by blanchet
three-line 'obtain' format for generated Isar proofs
2014-08-28, by blanchet
tuned;
2014-08-28, by wenzelm
more liberal embedded "text", which includes cartouches;
2014-08-28, by wenzelm
intern xthm only once;
2014-08-28, by wenzelm
tuned terminology
2014-08-28, by blanchet
moved new para to right section of NEWS
2014-08-28, by blanchet
minor NEWS fix
2014-08-28, by blanchet
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
2014-08-28, by blanchet
added 'OLD_' prefix in front of old solvers
2014-08-28, by blanchet
updated NEWS
2014-08-28, by blanchet
renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28, by blanchet
updated NEWS
2014-08-28, by blanchet
prefixed all old SMT commands, attributes, etc., with 'old_'
2014-08-28, by blanchet
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
2014-08-28, by blanchet
renaming theory 'Old_SMT'
2014-08-28, by blanchet
moved old setup for SMT out
2014-08-28, by blanchet
moved old 'smt' method out of 'Main'
2014-08-28, by blanchet
reintroduced two-line-per-inference Isar proof format
2014-08-28, by blanchet
removed needless, and for (newer versions of?) Haskell problematic code equations
2014-08-28, by blanchet
removed obsolete RC tags;
2014-08-27, by wenzelm
merged
2014-08-27, by wenzelm
Added tag Isabelle2014 for changeset 8f4a332500e4
2014-08-27, by wenzelm
merged
2014-08-27, by wenzelm
more explicit Method.modifier with reported position;
2014-08-27, by wenzelm
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
2014-08-27, by wenzelm
added ML antiquotation @{source} for Symbol_Pos.source;
2014-08-27, by wenzelm
tuned signature;
2014-08-25, by wenzelm
removed not so interesting 'set_empty'
2014-08-27, by blanchet
avoid 'PolyML.makestring'
2014-08-27, by blanchet
introduce real_of typeclass for real :: 'a => real
2014-08-25, by hoelzl
added lemmas
2014-08-25, by nipkow
better linarith support for floor, ceiling, natfloor, and natceiling
2014-08-19, by hoelzl
add testing framework for generated code
2014-08-25, by Andreas Lochbihler
correct code equation for term_of on integer
2014-08-25, by Andreas Lochbihler
merged
2014-08-25, by Andreas Lochbihler
add code equation for term_of on integer
2014-08-22, by Andreas Lochbihler
added lemmas contributed by Rene Thiemann
2014-08-22, by blanchet
attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
2014-08-22, by wenzelm
tuned whitespace;
2014-08-22, by wenzelm
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
2014-08-22, by wenzelm
merged
2014-08-22, by wenzelm
made SML/NJ happy;
2014-08-22, by wenzelm
clarified Method.section: explicit declaration with static closure;
2014-08-21, by wenzelm
tuned signature -- define some elementary operations earlier;
2014-08-21, by wenzelm
discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;
2014-08-21, by wenzelm
tuned;
2014-08-21, by wenzelm
tuned;
2014-08-21, by wenzelm
tuned;
2014-08-21, by wenzelm
generic euclidean algorithm (due to Manuel Eberl)
2014-08-22, by haftmann
integrated appendix theory into main theory;
2014-08-21, by haftmann
dropped dead file
2014-08-21, by haftmann
fix tactic failure with rel_induct0
2014-08-21, by desharna
added jdk-8u20 (inactive);
2014-08-20, by wenzelm
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
2014-08-20, by wenzelm
support for declaration within token source;
2014-08-20, by wenzelm
more uniform data slot;
2014-08-20, by wenzelm
default command position is only valid for default text chunk (amending dcb758188aa6);
2014-08-20, by wenzelm
tuned -- more total;
2014-08-20, by wenzelm
tuned;
2014-08-20, by wenzelm
support for nested Token.src within Token.T;
2014-08-20, by wenzelm
tuned signature -- moved type src to Token, without aliases;
2014-08-19, by wenzelm
merged
2014-08-19, by wenzelm
clarified modules;
2014-08-19, by wenzelm
added PARALLEL_ALLGOALS convenience;
2014-08-19, by wenzelm
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
2014-08-19, by wenzelm
tuned signature;
2014-08-19, by wenzelm
more compact datatypes;
2014-08-19, by wenzelm
tuned;
2014-08-19, by wenzelm
clarifed Method.evaluate: turn text into semantic method (like Basic);
2014-08-19, by wenzelm
simplified type Proof.method;
2014-08-19, by wenzelm
more general dummy: may contain "parked arguments", for example;
2014-08-18, by wenzelm
document 'ctr_transfer'
2014-08-19, by desharna
generate 'ctr_transfer' for (co)datatypes
2014-08-19, by desharna
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-08-19, by Andreas Lochbihler
Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)
2014-08-19, by Andreas Lochbihler
reduced dependency on 'Datatype' theory and ML module
2014-08-19, by blanchet
removed Z3 3.2, now superseded by Z3 4.3
2014-08-19, by blanchet
avoid old 'smt' method in examples
2014-08-19, by blanchet
robustified tactics
2014-08-19, by blanchet
tuning
2014-08-19, by blanchet
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
2014-08-19, by blanchet
documented slight incompatibility in NEWS
2014-08-19, by blanchet
removed junk
2014-08-18, by blanchet
updated docs
2014-08-18, by blanchet
set attributes on 'set_cases' theorem
2014-08-18, by blanchet
cleaned up derivation of 'sset_induct'
2014-08-18, by blanchet
tuning
2014-08-18, by blanchet
added collection theorem for consistency and convenience
2014-08-18, by blanchet
reordered some (co)datatype property names for more consistency
2014-08-18, by blanchet
document 'map_cong_simp'
2014-08-18, by desharna
generate 'map_cong_simp' for BNFs
2014-08-18, by desharna
merged
2014-08-18, by wenzelm
merged;
2014-08-18, by wenzelm
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Isabelle2014
2014-08-18, by wenzelm
updated to jdk-7u67;
2014-08-18, by wenzelm
postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
2014-08-17, by wenzelm
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
2014-08-15, by wenzelm
added option editor_syslog_limit;
2014-08-13, by wenzelm
tuned;
2014-08-13, by wenzelm
updated to cygwin-20140813 -- some version after 1.7.31-3;
2014-08-13, by wenzelm
document 'inj_map_strong'
2014-08-18, by desharna
generate 'inj_map_strong' for BNFs
2014-08-18, by desharna
note 'inj_map' more often
2014-08-18, by desharna
generate property 'rel_mono_strong' for BNFs
2014-08-18, by desharna
renamed 'rel_mono_strong' to 'rel_mono_strong0'
2014-08-18, by desharna
use 'image_mset' as BNF map function
2014-08-17, by blanchet
made SML/NJ happy;
2014-08-17, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
clarified order of rules;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
clarified order of arith rules;
2014-08-16, by wenzelm
clarified order of rules for match_tac/resolve_tac;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
modernized module name and setup;
2014-08-16, by wenzelm
updated syntax for localized commands;
2014-08-16, by wenzelm
updated documentation concerning 'named_theorems';
2014-08-16, by wenzelm
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
2014-08-16, by wenzelm
more informative Token.Name with history of morphisms;
2014-08-15, by wenzelm
merged
2014-08-14, by wenzelm
more informative Token.Fact: retain name of dynamic fact (without selection);
2014-08-14, by wenzelm
localized command 'method_setup' and 'attribute_setup';
2014-08-14, by wenzelm
T1 font encoding with searchable underscore (requires proper cm-super fonts);
2014-08-14, by wenzelm
prefer high-level change of \isabellestyle;
2014-08-14, by wenzelm
tuned;
2014-08-14, by wenzelm
tuned;
2014-08-14, by wenzelm
tuned signature;
2014-08-14, by wenzelm
localized method definitions (see also f14c1248d064);
2014-08-14, by wenzelm
tuned signature -- prefer self-contained user-space tool;
2014-08-14, by wenzelm
document property 'rel_map'
2014-08-14, by desharna
generate 'rel_map' theorem for BNFs
2014-08-14, by desharna
tuned;
2014-08-13, by wenzelm
merged
2014-08-13, by wenzelm
tuned signature -- proper Local_Theory.add_thms_dynamic;
2014-08-13, by wenzelm
transfer result of Global_Theory.add_thms_dynamic to context stack;
2014-08-13, by wenzelm
localized attribute definitions;
2014-08-13, by wenzelm
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
2014-08-13, by wenzelm
clarified terminology: first is top (amending d110b0d1bc12);
2014-08-13, by wenzelm
tuned whitespace;
2014-08-13, by wenzelm
tuned comments;
2014-08-13, by wenzelm
add algebraic type class instances for Enum.finite* types
2014-08-13, by Andreas Lochbihler
Quickcheck_Types is no longer needed due to 51aa30c9ee4e
2014-08-13, by Andreas Lochbihler
clarified focus and key handling -- more like SideKick;
2014-08-12, by wenzelm
merged
2014-08-12, by wenzelm
tuned signature according to Scala version -- prefer explicit argument;
2014-08-12, by wenzelm
tuned signature;
2014-08-12, by wenzelm
generic process wrapping in Prover;
2014-08-12, by wenzelm
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
2014-08-12, by wenzelm
allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
2014-08-12, by wenzelm
more frugal standard message properties;
2014-08-12, by wenzelm
tuned;
2014-08-12, by wenzelm
clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12, by wenzelm
maintain Command_Range position as in ML;
2014-08-12, by wenzelm
more compact representation of special string values;
2014-08-12, by wenzelm
separate Java FX modules -- no need to include jfxrt.jar by default;
2014-08-12, by wenzelm
tuned signature;
2014-08-12, by wenzelm
tuned signature;
2014-08-12, by wenzelm
separate module Command_Span: mostly syntactic representation;
2014-08-12, by wenzelm
tuned signature;
2014-08-11, by wenzelm
clarified Command_Span in accordance to Scala (see also c2c1e5944536);
2014-08-11, by wenzelm
tuned output, in accordance to transaction name in ML;
2014-08-11, by wenzelm
more explicit type Span in Scala, according to ML version;
2014-08-11, by wenzelm
clarified modules;
2014-08-11, by wenzelm
clarified signature: entity serial number is not position id;
2014-08-11, by wenzelm
avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;
2014-08-12, by blanchet
improved unfolding of 'let's
2014-08-12, by blanchet
tuned whitespace
2014-08-12, by blanchet
less aggressive unfolding; removed debugging;
2014-08-12, by blanchet
document property 'set_cases'
2014-08-12, by desharna
generate 'set_cases' theorem for (co)datatypes
2014-08-12, by desharna
document property 'set_intros'
2014-08-12, by desharna
generate 'set_intros' theorem for (co)datatypes
2014-08-12, by desharna
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
2014-08-11, by traytel
reduced warnings;
2014-08-10, by wenzelm
some localization;
2014-08-10, by wenzelm
support aliases within the facts space;
2014-08-10, by wenzelm
support for named collections of theorems in canonical order;
2014-08-10, by wenzelm
insist in proper 'document_files';
2014-08-10, by wenzelm
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
2014-08-10, by wenzelm
tuned -- eliminated redundant check (see 1f77110c94ef);
2014-08-10, by wenzelm
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-08-10, by wenzelm
updated URL (anticipate merge with 85b8cc142384);
2014-08-10, by wenzelm
Added tag Isabelle2014-RC3 for changeset 91e188508bc9
2014-08-10, by wenzelm
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
2014-08-10, by wenzelm
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
2014-08-10, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned comments;
2014-08-09, by wenzelm
clarified synchronized scope;
2014-08-09, by wenzelm
tuned comments;
2014-08-09, by wenzelm
application manifest for Windows 8/8.1 dpi scaling;
2014-08-08, by wenzelm
observe context visibility -- less redundant warnings;
2014-08-08, by wenzelm
improved monitor panel;
2014-08-08, by wenzelm
protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
2014-08-05, by wenzelm
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
2014-08-05, by wenzelm
obsolete (see f7700146678d);
2014-08-05, by wenzelm
tuned proofs -- fewer warnings;
2014-08-05, by wenzelm
clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
2014-08-05, by wenzelm
avoid duplication of warnings stemming from simp/intro declarations etc.;
2014-08-05, by wenzelm
tuned proofs;
2014-08-05, by wenzelm
restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
2014-08-05, by wenzelm
tuned;
2014-08-05, by wenzelm
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
2014-08-05, by wenzelm
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
2014-08-05, by wenzelm
even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);
2014-08-04, by wenzelm
tuned;
2014-08-04, by wenzelm
tuned;
2014-08-04, by wenzelm
Added tag Isabelle2014-RC2 for changeset ee908fccabc2
2014-08-04, by wenzelm
more user aliases;
2014-08-04, by wenzelm
registered Haskabelle-2014
2014-08-04, by noschinl
tuned, so codegen runs with current isabelle again
2014-08-01, by Lars Noschinski
tuned whitespace;
2014-08-03, by wenzelm
more robust popup geometry vs. formatted margin;
2014-08-03, by wenzelm
tuned message;
2014-08-03, by wenzelm
updated URL;
2014-08-02, by wenzelm
tuned;
2014-08-02, by wenzelm
updated URL;
2014-08-02, by wenzelm
more emphatic warning via error_message (violating historic TTY protocol);
2014-08-02, by wenzelm
proper priority for error over warning also for node_status (see 9c5220e05e04);
2014-08-02, by wenzelm
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
2014-08-02, by wenzelm
always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
2014-08-02, by wenzelm
tuned output;
2014-08-02, by wenzelm
prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
2014-08-01, by wenzelm
careful when calling 'Thm.proof_body_of' -- it can throw exceptions
2014-08-01, by blanchet
removed unused stuff;
2014-08-01, by wenzelm
agree on keyword categories with ML;
2014-08-01, by wenzelm
more keyword categories (as in ML);
2014-08-01, by wenzelm
prefer dynamic ML_print_depth if context happens to be available;
2014-07-31, by wenzelm
completion popup supports both ENTER and TAB (default);
2014-07-31, by wenzelm
clarified compile-time use of ML_print_depth;
2014-07-31, by wenzelm
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-07-31, by wenzelm
correctly resolve selector names in default value equations
2014-07-30, by blanchet
update documentation for Lifting/Transfer
2014-07-30, by kuncar
add Isabelle Datatype Manual to the bibliography
2014-07-30, by kuncar
CONTRIBUTORS;
2014-07-30, by wenzelm
NEWS
2014-07-30, by kuncar
better ordering of positive_integral renaming to nn_integral in NEWS
2014-07-29, by hoelzl
made tactic more robust w.r.t. dead variables; tuned;
2014-07-28, by desharna
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-27, by blanchet
some actual workaround to remove document nodes;
2014-07-28, by wenzelm
Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
2014-07-27, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned
2014-08-09, by nipkow
add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
2014-08-08, by Andreas Lochbihler
tuned
2014-08-08, by nipkow
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-08-07, by blanchet
generate nicer 'set' theorems for (co)datatypes
2014-08-07, by blanchet
compile
2014-08-07, by blanchet
took out test driver
2014-08-07, by blanchet
make TPTP tools work on polymorphic (TFF1) problems as well
2014-08-07, by blanchet
put comments between TPTP lines to comply with TPTP BNF
2014-08-07, by blanchet
test driver
2014-08-07, by blanchet
treat variables as frees in 'conjecture's
2014-08-07, by blanchet
support TFF1 in TPTP parser/interpreter
2014-08-07, by blanchet
tuning
2014-08-07, by blanchet
tuned
2014-08-07, by traytel
tuned
2014-08-07, by nipkow
tuned
2014-08-07, by nipkow
merged
2014-08-06, by traytel
handle deep nesting in N2M
2014-08-06, by traytel
made tactic more robust
2014-08-06, by traytel
added lemma
2014-08-06, by nipkow
replaced misleading - by _
2014-08-06, by nipkow
more correct clique computation for N2M
2014-08-05, by blanchet
regenerated ML-Lex/Yacc files
2014-08-05, by blanchet
correctly interpret arithmetic types
2014-08-05, by blanchet
added 'datatype_compat' tests
2014-08-05, by blanchet
tuning whitespace
2014-08-05, by blanchet
tuned skolemization
2014-08-05, by blanchet
rationalize Skolem names
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned code
2014-08-05, by blanchet
don't rename variables which will be renamed later anyway
2014-08-05, by blanchet
normalize skolem argument variable names so that they coincide when taking the conjunction
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned comments
2014-08-04, by blanchet
deal with E definitions
2014-08-04, by blanchet
updated 'compress' docs
2014-08-04, by blanchet
cleaner 'compress' option
2014-08-04, by blanchet
renamed 'sh_minimize' to 'minimize'; compile;
2014-08-04, by blanchet
restored more sorting
2014-08-04, by blanchet
tuned terminology (cf. 'isar_proofs' option)
2014-08-04, by blanchet
sort facts in minimizer as well
2014-08-04, by blanchet
default on 'metis' for ATPs if preplaying is disabled
2014-08-04, by blanchet
more informative preplay failures
2014-08-04, by blanchet
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-04, by blanchet
slightly earlier exit from preplaying
2014-08-04, by blanchet
honor 'dont_minimize' option when preplaying one-liner proof
2014-08-04, by blanchet
Metis is being used to emulate E steps;
2014-06-22, by sultana
updated application of print_tac to take context parameter;
2014-06-22, by sultana
better duplicate detection
2014-08-02, by blanchet
normalize conjectures vs. negated conjectures when comparing terms
2014-08-01, by blanchet
tweaked 'clone' formula detection
2014-08-01, by blanchet
fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01, by blanchet
centralized boolean simplification so that e.g. LEO-II benefits from it
2014-08-01, by blanchet
careful when compressing 'obtains'
2014-08-01, by blanchet
better handling of variable names
2014-08-01, by blanchet
try to get rid of skolems first
2014-08-01, by blanchet
nicer generated variable names
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
no need to 'obtain' variables not in formula
2014-08-01, by blanchet
more precise handling of LEO-II skolemization
2014-08-01, by blanchet
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
peek instead of joining -- is perhaps less risky
2014-08-01, by blanchet
export ML function
2014-08-01, by blanchet
compile
2014-08-01, by blanchet
removed 'metisFT' support in Mirabelle
2014-08-01, by blanchet
removed Mirabelle minimization code
2014-08-01, by blanchet
modernized Mirabelle (a bit) and made it compile
2014-08-01, by blanchet
restored a bit of laziness
2014-08-01, by blanchet
reorder quantifiers to ease Z3 skolemization
2014-08-01, by blanchet
tuned order of arguments
2014-08-01, by blanchet
tuned name context code
2014-08-01, by blanchet
tuned whitespace
2014-08-01, by blanchet
more rational unskolemizing of names
2014-08-01, by blanchet
added appropriate method for skolemization of Z3 steps to the mix
2014-08-01, by blanchet
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
2014-08-01, by blanchet
honor 'try0' also for one-liners
2014-08-01, by blanchet
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01, by blanchet
further minimize one-liner
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
eliminated needlessly complex message tail
2014-08-01, by blanchet
updated NEWS
2014-08-01, by blanchet
update documentation after removal of 'min' subcommand
2014-08-01, by blanchet
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01, by blanchet
rationalized preplaying by eliminating (now superfluous) laziness
2014-08-01, by blanchet
removed proof methods as provers from docs
2014-08-01, by blanchet
simplified minimization logic
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
remove lambda-lifting related assumptions from generated Isar proofs
2014-08-01, by blanchet
whitespace tuning
2014-08-01, by blanchet
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
2014-08-01, by blanchet
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
2014-08-01, by blanchet
simplified tactics slightly
2014-07-31, by traytel
cascading timeout in parallel evaluation, to rapidly find optimum
2014-07-31, by blanchet
put faster proof methods first
2014-07-30, by blanchet
use parallel preplay machinery also for one-line proofs
2014-07-30, by blanchet
updated docs
2014-07-30, by blanchet
always minimize Sledgehammer results by default
2014-07-30, by blanchet
tuned ML function name
2014-07-30, by blanchet
reduced preplay timeout to 1 s
2014-07-30, by blanchet
added more proof methods for one-liners
2014-07-30, by blanchet
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
2014-07-30, by blanchet
Improving robustness and indentation corrections.
2014-07-30, by fleury
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
2014-07-30, by fleury
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
2014-07-30, by fleury
Whitespace and indentation correction.
2014-07-30, by fleury
Simplifying the labels in the proof of the SMT solver veriT.
2014-07-30, by fleury
Changing ~ into - for unuary minus (not supported by veriT)
2014-07-30, by fleury
imported patch satallax_skolemization_in_tree_part
2014-07-30, by fleury
imported patch hilbert_choice_support
2014-07-30, by fleury
veriT changes for lifted terms, and ite_elim rules.
2014-07-30, by fleury
imported patch satallax_proof_support_Sledgehammer
2014-07-30, by fleury
Basic support for the higher-order ATP Satallax.
2014-07-30, by fleury
Subproofs for the SMT solver veriT.
2014-07-30, by fleury
Basic support for the SMT prover veriT.
2014-07-30, by fleury
removing the '= True' generated by Leo-II.
2014-07-30, by fleury
Skolemization support for leo-II and Zipperposition.
2014-07-30, by fleury
document property 'set_induct'
2014-07-30, by desharna
generate 'set_induct' theorem for codatatypes
2014-07-30, by desharna
also try 'metis' with 'full_types'
2014-07-30, by blanchet
header tuning
2014-07-29, by blanchet
correctly translate THF functions from terms to types
2014-07-28, by blanchet
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-27, by blanchet
back to post-release mode -- after fork point;
2014-07-27, by wenzelm
tuned;
2014-07-27, by wenzelm
tuned;
2014-07-27, by wenzelm
no -optimise -- produces bad bytecode;
2014-07-26, by wenzelm
output state first -- avoid fluctuation wrt. warnings, errors, etc.;
2014-07-26, by wenzelm
tuned comment;
2014-07-25, by wenzelm
updated to polyml-5.5.2-1 which addresses two hard crashes;
2014-07-25, by wenzelm
updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;
2014-07-25, by wenzelm
added more functions and lemmas
2014-07-25, by nipkow
proper mkdir;
2014-07-25, by wenzelm
proper option -O;
2014-07-25, by wenzelm
some reshuffling of Poly/ML version to evade failing tests;
2014-07-25, by wenzelm
old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
2014-07-25, by wenzelm
proper volume name, such that background image is found in /Volumes/Isabelle/.background;
2014-07-25, by wenzelm
tuned;
2014-07-25, by wenzelm
tuned message;
2014-07-25, by wenzelm
setup for drag-and-drop DMG;
2014-07-25, by wenzelm
merge
2014-07-25, by blanchet
reordered provers
2014-07-25, by blanchet
compile
2014-07-25, by blanchet
faster minimization by not adding facts that are already in the simpset
2014-07-25, by blanchet
added missing facts to proof method
2014-07-25, by blanchet
don't lose 'minimize' flag before it reaches Isar proof text generation
2014-07-25, by blanchet
tuning
2014-07-25, by blanchet
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
2014-07-25, by blanchet
compile
2014-07-25, by blanchet
more robustness in Isar proof construction
2014-07-25, by blanchet
tuning
2014-07-25, by blanchet
merged
2014-07-24, by wenzelm
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
2014-07-24, by wenzelm
tuned code
2014-07-24, by blanchet
having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations
2014-07-24, by kuncar
store explicitly quotient types with no_code => more precise registration of code equations
2014-07-24, by kuncar
don't needlessly regenerate entire file when the time stamps are equal
2014-07-24, by blanchet
eliminated source of 'DUP's in MaSh
2014-07-24, by blanchet
fixed sorting (broken since 9cc802a8ab06)
2014-07-24, by blanchet
reenabled MaSh for Isabelle2014 release (hopefully)
2014-07-24, by blanchet
beware of duplicate fact names
2014-07-24, by blanchet
refined filter for ATP steps to avoid 'have True' steps in E proofs
2014-07-24, by blanchet
filter out 'theory(...)' from dependencies early on
2014-07-24, by blanchet
introduce fact chaining also under first step
2014-07-24, by blanchet
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
2014-07-24, by blanchet
merged
2014-07-24, by wenzelm
proper perl;
2014-07-24, by wenzelm
less warnings -- ignore potential prover startup/shutdown races;
2014-07-24, by wenzelm
tuned spelling;
2014-07-24, by wenzelm
further distinction of Isabelle distribution: alert for identified release candidates;
2014-07-24, by wenzelm
updated to scala-2.11.2;
2014-07-24, by wenzelm
clarified file names;
2014-07-24, by wenzelm
less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;
2014-07-24, by wenzelm
tuned imports;
2014-07-24, by wenzelm
proper scope of comments;
2014-07-24, by wenzelm
make SML/NJ happy;
2014-07-24, by wenzelm
prevent beta-contraction in proving extra assumptions for abs_eq
2014-07-24, by kuncar
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-07-24, by wenzelm
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
2014-07-24, by wenzelm
tuned;
2014-07-24, by wenzelm
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
2014-07-24, by wenzelm
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
2014-07-24, by wenzelm
stick to external proofs when invoking E, because they are more detailed and do not merge steps
2014-07-24, by blanchet
more robust handling of types for skolems (modeled as Frees)
2014-07-24, by blanchet
tuning
2014-07-24, by blanchet
repaired named derivations
2014-07-24, by blanchet
use the noted theorems in 'BNF_Comp'
2014-07-24, by blanchet
use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-24, by blanchet
use termtab instead of (perhaps overly sensitive) thmtab
2014-07-24, by blanchet
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
2014-07-24, by blanchet
tuned message;
2014-07-23, by wenzelm
added action "isabelle.options" (despite problems with initial window size);
2014-07-23, by wenzelm
more official Thy_Info.script_thy;
2014-07-23, by wenzelm
more frugal edits;
2014-07-23, by wenzelm
enable hires explictly, as seen for other high-end Java applications on the Web;
2014-07-23, by wenzelm
more markup;
2014-07-23, by wenzelm
another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;
2014-07-23, by wenzelm
more frugal edits;
2014-07-23, by wenzelm
more explicit treatment of cleared nodes (removal is implicit);
2014-07-23, by wenzelm
clarified display;
2014-07-23, by wenzelm
more workarounds for scalac;
2014-07-23, by wenzelm
clarified display;
2014-07-23, by wenzelm
avoid redundant data structure;
2014-07-23, by wenzelm
more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-07-23, by wenzelm
tuned;
2014-07-23, by wenzelm
tuned comments;
2014-07-23, by wenzelm
clarified module name: facilitate alternative GUI frameworks;
2014-07-23, by wenzelm
proper change of perspective for removed nodes (stemming from closed buffers);
2014-07-23, by wenzelm
tuned signature;
2014-07-23, by wenzelm
some robustification of console output;
2014-07-22, by wenzelm
updated ErrorList.jar;
2014-07-22, by wenzelm
discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
2014-07-22, by wenzelm
evade problems with MikTeX on Windows;
2014-07-22, by wenzelm
tuned messages;
2014-07-22, by wenzelm
support multiple selected print operations instead of slightly odd "menu";
2014-07-22, by wenzelm
more default imports;
2014-07-22, by wenzelm
no keyword completion within word context -- especially avoid its odd visual rendering;
2014-07-22, by wenzelm
merged
2014-07-22, by Andreas Lochbihler
merged
2014-07-21, by Andreas Lochbihler
add parametricity lemmas
2014-07-21, by Andreas Lochbihler
add lemma
2014-07-21, by Andreas Lochbihler
merged
2014-07-21, by wenzelm
refer to Simplifier Trace panel on first invocation;
2014-07-21, by wenzelm
removed unused markup (cf. 2f7d91242b99);
2014-07-21, by wenzelm
regular message to refer to Simplifier Trace panel (unused);
2014-07-21, by wenzelm
proper Swing buttons instead of active areas within text (by Lars Hupel);
2014-07-21, by wenzelm
misc tuning and simplification;
2014-07-21, by wenzelm
clarified "simp_trace_new" and corresponding isar-ref section;
2014-07-21, by wenzelm
more on "Simplifier trace" (by Lars Hupel);
2014-07-21, by wenzelm
always complete explicit symbols;
2014-07-21, by wenzelm
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
2014-07-21, by wenzelm
updated to jdk-7u65;
2014-07-21, by wenzelm
regression test for datatypes defined in IsaFoR
2014-07-21, by traytel
ghc mac installation repaired; test back on.
2014-07-21, by kleing
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-20, by wenzelm
updated to jdk-8u11 (inactive);
2014-07-20, by wenzelm
avoid delay_load overrun;
2014-07-20, by wenzelm
provide explicit options file -- avoid multiple Scala/JVM invocation;
2014-07-20, by wenzelm
check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
2014-07-20, by wenzelm
attempt to run without ISABELLE_GHC setting again on mac-poly
2014-07-19, by kleing
apparently, setting ISABELLE_GHC makes ghc unusable
2014-07-19, by kleing
reverse induction over nonempty lists
2014-07-19, by haftmann
more appropriate postprocessing of rational numbers: extract sign to front of fraction
2014-07-19, by haftmann
doc fixes (contributed by Christian Sternagel)
2014-07-19, by blanchet
made SML/NJ happier
2014-07-19, by blanchet
avoid duplicate fact name
2014-07-18, by kleing
afp-poly runs on macbroy2 (different ghc)
2014-07-18, by kleing
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
2014-07-18, by nipkow
tuned
2014-07-18, by nipkow
register tree with datatype_compat ot support QuickCheck
2014-07-17, by hoelzl
fix bug caused by bad context
2014-07-17, by desharna
add mk_Trueprop_mem utility function
2014-07-17, by desharna
disabled MaSh for the Isabelle2014 release, due to a couple of issues
2014-07-16, by blanchet
refactor commonly used functions
2014-07-16, by desharna
document property 'rel_sel'
2014-07-16, by desharna
generate 'rel_sel' theorem for (co)datatypes
2014-07-16, by desharna
fix rel_cases
2014-07-16, by desharna
made SML/NJ happier
2014-07-15, by blanchet
add ISABELLE_GHC settings for isatest
2014-07-15, by kleing
mira.py: building jEdit plugin is required for makeall
2014-07-14, by noschinl
took out 'rel_cases' for now because of failing tactic
2014-07-15, by blanchet
record MaSh algorithm in spying data
2014-07-15, by blanchet
tuned whitespace (also in strings)
2014-07-15, by blanchet
also learn when 'fact_filter =' is set explicitly
2014-07-15, by blanchet
no warning in case MaSh is disabled
2014-07-15, by blanchet
don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
2014-07-15, by blanchet
no need for 'mash' subdirectory after removal of Python program
2014-07-15, by blanchet
fix typo
2014-07-14, by panny
throw error for bad input
2014-07-14, by panny
catch "not found" case
2014-07-14, by panny
merge
2014-07-12, by blanchet
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
2014-07-12, by blanchet
tuning
2014-07-12, by blanchet
made SML/NJ happier
2014-07-12, by blanchet
reactivate session Quickcheck_Examples
2014-07-11, by Andreas Lochbihler
adapt and reactivate Quickcheck_Types and add two test cases
2014-07-11, by Andreas Lochbihler
more docs
2014-07-11, by blanchet
lambda-lifting for Z3 Isar proofs
2014-07-10, by blanchet
append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)
2014-07-10, by blanchet
avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)
2014-07-10, by blanchet
merged
2014-07-09, by nipkow
added lemmas
2014-07-09, by nipkow
improved docs
2014-07-09, by blanchet
made SML/NJ happier
2014-07-09, by blanchet
got rid of a pointer equality
2014-07-09, by blanchet
get rid of some pointer equalities
2014-07-09, by blanchet
tuned terminology
2014-07-09, by blanchet
improvements to the machine learning algos (due to Cezary K.)
2014-07-09, by blanchet
added lemma
2014-07-07, by nipkow
refactor some tactics
2014-07-07, by desharna
refactor some tactics
2014-07-07, by desharna
add helper function map_prod
2014-07-07, by desharna
document property 'rel_cases'
2014-07-07, by desharna
generate 'rel_cases' theorem for (co)datatypes
2014-07-07, by desharna
update for release;
2014-07-05, by wenzelm
Added tag Isabelle2014-RC0 for changeset 251ef0202e71
2014-07-05, by wenzelm
merged
2014-07-05, by wenzelm
modernized definitions;
2014-07-05, by wenzelm
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
2014-07-05, by wenzelm
CONTRIBUTORS
2014-07-05, by haftmann
refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply;
2014-07-05, by haftmann
misc tuning for release;
2014-07-05, by wenzelm
tuned;
2014-07-05, by wenzelm
NEWS
2014-07-05, by haftmann
prefer ac_simps collections over separate name bindings for add and mult
2014-07-05, by haftmann
added Tom's hyp_subst update
2014-07-05, by kleing
reduced name variants for assoc and commute on plus and mult
2014-07-04, by haftmann
tuned;
2014-07-04, by wenzelm
insist in explicit overloading;
2014-07-04, by wenzelm
more uniform names;
2014-07-04, by wenzelm
misc tuning for release;
2014-07-04, by wenzelm
revived unchecked theory (see cebaf814ca6e);
2014-07-04, by wenzelm
suppress completion of obscure keyword;
2014-07-04, by wenzelm
tuned;
2014-07-04, by wenzelm
misc tuning for release;
2014-07-04, by wenzelm
NEWS;
2014-07-04, by wenzelm
Tail recursion no longer supported by "function".
2014-07-03, by nipkow
merged
2014-07-03, by haftmann
weaker assumption for "list_emb_trans"; added lemma
2014-07-03, by Christian Sternagel
added monotonicity lemma for list embedding
2014-07-03, by Christian Sternagel
no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
2014-07-03, by Christian Sternagel
renamed "list_hembeq" into slightly shorter "list_emb"
2014-07-03, by Christian Sternagel
misc tuning;
2014-07-03, by wenzelm
merge
2014-07-03, by desharna
document property 'rel_intros'
2014-07-03, by desharna
generate 'rel_intros' theorem for (co)datatypes
2014-07-03, by desharna
Hypsubst preserves equality hypotheses
2014-06-11, by Thomas Sewell
tuned grammar and spelling (cf. 0cf15843b82f);
2014-07-02, by wenzelm
document property 'corec_code'
2014-07-02, by desharna
generate 'corec_code' theorem for codatatypes
2014-07-02, by desharna
modernized definitions;
2014-07-02, by wenzelm
misc tuning and clarification;
2014-07-02, by wenzelm
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
2014-07-02, by wenzelm
optional exit hook for theory-like targets
2014-07-02, by haftmann
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
2014-07-02, by haftmann
centralized (ad-hoc) switching of targets in named_target.ML
2014-07-02, by haftmann
less
more
|
(0)
-30000
-10000
-4096
+4096
+10000
tip