| 2016-01-16 |
wenzelm |
keep src/Doc;
|
changeset |
files
|
| 2016-01-16 |
wenzelm |
tuned URLs according to website;
|
changeset |
files
|
| 2016-01-16 |
wenzelm |
more symbols;
|
changeset |
files
|
| 2016-01-16 |
wenzelm |
tuned message;
|
changeset |
files
|
| 2016-01-16 |
wenzelm |
tuned message;
|
changeset |
files
|
| 2016-01-15 |
wenzelm |
Added tag Isabelle2016-RC1 for changeset 155d30f721dd
|
changeset |
files
|
| 2016-01-15 |
wenzelm |
misc updates and tuning;
|
changeset |
files
|
| 2016-01-15 |
wenzelm |
misc updates and tuning;
|
changeset |
files
|
| 2016-01-15 |
wenzelm |
misc updates and tuning;
|
changeset |
files
|
| 2016-01-15 |
immler |
continuity of parameterized integral; easier-to-apply formulation of rules
|
changeset |
files
|
| 2016-01-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 2016-01-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 2016-01-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 2016-01-14 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
removed dead code;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
tuned syntax;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
isabelle update_cartouches -c -t;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
eliminated spurious Unicode;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
clarified example;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
updated section on "Overloaded constant definitions";
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
more doc content;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
tuned;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
removed old 'defs' command;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
more doc content;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
merged;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
proper relative symlink;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
tuned;
|
changeset |
files
|
| 2016-01-13 |
wenzelm |
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
|
changeset |
files
|
| 2016-01-13 |
nipkow |
merged
|
changeset |
files
|
| 2016-01-13 |
nipkow |
tuned layout
|
changeset |
files
|
| 2016-01-13 |
blanchet |
updated NEWS
|
changeset |
files
|
| 2016-01-13 |
blanchet |
generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
more good NEWS;
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
merged
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
updated old screenshots, added new screenshots;
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
more explicit errors for control symbols that are left-over after Markdown parsing;
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
removed in anticipation of c92d82c3f41b -- demolition after renovation;
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-12 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
clarified axiomatization versus definitions;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-11 |
wenzelm |
eliminated old defs;
|
changeset |
files
|
| 2016-01-12 |
eberlm |
Deleted problematic code equation in Binomial temporarily.
|
changeset |
files
|
| 2016-01-12 |
Andreas Lochbihler |
add reference
|
changeset |
files
|
| 2016-01-12 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| 2016-01-12 |
Andreas Lochbihler |
add BNF instance for Dlist
|
changeset |
files
|
| 2016-01-12 |
paulson |
crediting LCP in CONTRIBUTORS
|
changeset |
files
|
| 2016-01-12 |
traytel |
more careful witness' type analysis
|
changeset |
files
|
| 2016-01-12 |
traytel |
removed outdated example
|
changeset |
files
|
| 2016-01-12 |
matichuk |
remove unused code
|
changeset |
files
|
| 2016-01-12 |
matichuk |
remove Eisbach's dependency on HOL
|
changeset |
files
|
| 2016-01-11 |
matichuk |
match method now makes proper use of context_tactic
|
changeset |
files
|
| 2016-01-11 |
paulson |
merged
|
changeset |
files
|