2012-11-06 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
2012-10-22 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
2012-10-22 |
wenzelm |
more detailed Prover IDE NEWS;
|
file |
diff |
annotate
|
2012-10-21 |
webertj |
merged
|
file |
diff |
annotate
|
2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
2012-10-20 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
2012-10-18 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
2012-10-16 |
wenzelm |
support for more informative errors in lazy enumerations;
|
file |
diff |
annotate
|
2012-10-12 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
2012-10-12 |
wenzelm |
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
|
file |
diff |
annotate
|
2012-10-11 |
haftmann |
simplified construction of fold combinator on multisets;
|
file |
diff |
annotate
|
2012-10-10 |
Andreas Lochbihler |
efficient construction of red black trees from sorted associative lists
|
file |
diff |
annotate
|
2012-10-08 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
2012-10-08 |
haftmann |
corrected NEWS
|
file |
diff |
annotate
|
2012-10-04 |
wenzelm |
some documentation of show_markup;
|
file |
diff |
annotate
|
2012-09-28 |
wenzelm |
smarter handling of tracing messages;
|
file |
diff |
annotate
|
2012-09-22 |
wenzelm |
some PIDE NEWS from this summer;
|
file |
diff |
annotate
|
2012-09-21 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
|
2012-09-20 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
|
file |
diff |
annotate
|
2012-09-15 |
haftmann |
typeclass formalising bounded subtraction
|
file |
diff |
annotate
|
2012-09-14 |
blanchet |
merged two commands
|
file |
diff |
annotate
|
2012-09-12 |
blanchet |
renamed "Ordinals_and_Cardinals" to "Cardinals"
|
file |
diff |
annotate
|
2012-09-10 |
wenzelm |
more explicit indication of legacy features;
|
file |
diff |
annotate
|
2012-09-07 |
haftmann |
lattice instances for option type
|
file |
diff |
annotate
|
2012-09-07 |
haftmann |
combinator Option.these
|
file |
diff |
annotate
|
2012-09-04 |
Christian Sternagel |
NEWS; CONTRIBUTORS
|
file |
diff |
annotate
|
2012-09-03 |
wenzelm |
"isabelle logo" produces EPS and PDF format simultaneously;
|
file |
diff |
annotate
|
2012-08-29 |
wenzelm |
provide polyml-5.4.1 as regular component;
|
file |
diff |
annotate
|
2012-08-29 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
2012-08-28 |
blanchet |
updated NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2012-08-27 |
wenzelm |
clarified "isabelle logo";
|
file |
diff |
annotate
|
2012-08-22 |
wenzelm |
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
|
file |
diff |
annotate
|
2012-08-17 |
wenzelm |
some explanations on isabelle components;
|
file |
diff |
annotate
|
2012-08-14 |
wenzelm |
support for 'typ' with explicit sort constraint;
|
file |
diff |
annotate
|
2012-08-08 |
wenzelm |
discontinued obsolete "isabelle makeall";
|
file |
diff |
annotate
|
2012-08-07 |
wenzelm |
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
|
file |
diff |
annotate
|
2012-08-06 |
wenzelm |
"isabelle options" prints Isabelle system options;
|
file |
diff |
annotate
|
2012-08-05 |
wenzelm |
more on isabelle mkroot;
|
file |
diff |
annotate
|
2012-08-03 |
wenzelm |
simplified custom document/build script, instead of old-style document/IsaMakefile;
|
file |
diff |
annotate
|
2012-07-31 |
wenzelm |
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
|
file |
diff |
annotate
|
2012-07-28 |
wenzelm |
discontinued obsolete Isabelle/build script;
|
file |
diff |
annotate
|
2012-07-28 |
wenzelm |
announce advanced support for Isabelle sessions and build management;
|
file |
diff |
annotate
|
2012-07-28 |
wenzelm |
discontinued special treatment of Proof General;
|
file |
diff |
annotate
|
2012-07-23 |
haftmann |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
file |
diff |
annotate
|
2012-07-22 |
haftmann |
NEWS
|
file |
diff |
annotate
|
2012-07-20 |
blanchet |
added MaSh to news
|
file |
diff |
annotate
|
2012-07-19 |
haftmann |
export code relatively to master directory
|
file |
diff |
annotate
|
2012-07-18 |
blanchet |
removed lie
|
file |
diff |
annotate
|
2012-07-18 |
blanchet |
doc updates
|
file |
diff |
annotate
|
2012-07-06 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2012-07-06 |
wenzelm |
discontinued obsolete attribute "COMP";
|
file |
diff |
annotate
|
2012-06-29 |
wenzelm |
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
|
file |
diff |
annotate
|
2012-06-25 |
wenzelm |
updated "isar-ref" manual, reduced remaining material in "ref" manual.
|
file |
diff |
annotate
|
2012-06-21 |
bulwahn |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2012-06-06 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
2012-06-04 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|
2012-05-29 |
bulwahn |
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
|
file |
diff |
annotate
|
2012-05-24 |
wenzelm |
discontinued support for Poly/ML 5.2.1;
|
file |
diff |
annotate
|
2012-05-23 |
wenzelm |
discontinued obsolete method fastsimp / tactic fast_simp_tac;
|
file |
diff |
annotate
|
2012-05-23 |
wenzelm |
merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
|
file |
diff |
annotate
|