| 2009-09-30 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-09-30 |
haftmann |
mandatory prefix where appropriate
|
file |
diff |
annotate
|
| 2009-09-29 |
wenzelm |
Synchronized and Unsynchronized;
|
file |
diff |
annotate
|
| 2009-09-25 |
haftmann |
NEWS; corrected spelling
|
file |
diff |
annotate
|
| 2009-09-22 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-09-21 |
haftmann |
added note on simp rules
|
file |
diff |
annotate
|
| 2009-09-21 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-09-19 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| 2009-09-22 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
file |
diff |
annotate
|
| 2009-09-18 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
file |
diff |
annotate
|
| 2009-09-18 |
haftmann |
INTER and UNION are mere abbreviations for INFI and SUPR
|
file |
diff |
annotate
|
| 2009-09-18 |
haftmann |
tuned NEWS, added CONTRIBUTORS
|
file |
diff |
annotate
|
| 2009-09-17 |
paulson |
NEWS: New method metisFT
|
file |
diff |
annotate
|
| 2009-09-16 |
haftmann |
Inter and Union are mere abbreviations for Inf and Sup; tuned
|
file |
diff |
annotate
|
| 2009-09-01 |
haftmann |
corrected spelling
|
file |
diff |
annotate
|
| 2009-09-01 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| 2009-08-31 |
krauss |
moved lemma Wellfounded.in_inv_image to Relation.thy
|
file |
diff |
annotate
|
| 2009-08-28 |
wenzelm |
discontinued Display.pretty_ctyp/cterm etc.;
|
file |
diff |
annotate
|
| 2009-08-28 |
wenzelm |
misc updates and tuning;
|
file |
diff |
annotate
|
| 2009-08-21 |
boehmes |
added Mirabelle to NEWS
|
file |
diff |
annotate
|
| 2009-08-11 |
wenzelm |
added PARALLEL_CHOICE, PARALLEL_GOALS;
|
file |
diff |
annotate
|
| 2009-08-04 |
wenzelm |
etc/components;
|
file |
diff |
annotate
|
| 2009-07-29 |
nipkow |
sos documentation
|
file |
diff |
annotate
|
| 2009-07-28 |
haftmann |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file |
diff |
annotate
|
| 2009-07-27 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| 2009-07-27 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2009-07-26 |
wenzelm |
tacticals FOCUS and FOCUS_PARAMS;
|
file |
diff |
annotate
|
| 2009-07-23 |
wenzelm |
Proper context for simpset_of, claset_of, clasimpset_of.
|
file |
diff |
annotate
|
| 2009-07-22 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-07-22 |
haftmann |
set intersection and union now named inter and union
|
file |
diff |
annotate
|
| 2009-07-22 |
wenzelm |
merged, resolving trivial conflict;
|
file |
diff |
annotate
|
| 2009-07-22 |
nipkow |
News
|
file |
diff |
annotate
|
| 2009-07-20 |
wenzelm |
Display.pretty_thm now requires a proper context;
|
file |
diff |
annotate
|
| 2009-07-20 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2009-07-14 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-07-14 |
haftmann |
refinement of lattice classes
|
file |
diff |
annotate
|
| 2009-07-19 |
wenzelm |
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
|
file |
diff |
annotate
|
| 2009-07-14 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2009-07-09 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| 2009-07-02 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| 2009-07-02 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 2009-06-30 |
hoelzl |
NEWS updated
|
file |
diff |
annotate
|
| 2009-06-29 |
hoelzl |
Implemented taylor series expansion for approximation
|
file |
diff |
annotate
|
| 2009-06-26 |
nipkow |
lcm abs lemmas
|
file |
diff |
annotate
|
| 2009-06-25 |
hoelzl |
NEWS updated
|
file |
diff |
annotate
|
| 2009-06-08 |
hoelzl |
Added new evaluator "approximate"
|
file |
diff |
annotate
|
| 2009-06-25 |
haftmann |
arbitrary farewell
|
file |
diff |
annotate
|
| 2009-06-24 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| 2009-06-23 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| 2009-06-19 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-06-19 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| 2009-06-19 |
nipkow |
NewNumberTheory
|
file |
diff |
annotate
|
| 2009-06-15 |
haftmann |
authentic syntax for Pow and image
|
file |
diff |
annotate
|
| 2009-06-13 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-06-13 |
haftmann |
quickcheck using generic code generator
|
file |
diff |
annotate
|
| 2009-06-10 |
wenzelm |
discontinued escaped symbols;
|
file |
diff |
annotate
|
| 2009-06-08 |
haftmann |
method linarith
|
file |
diff |
annotate
|
| 2009-05-31 |
wenzelm |
removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
|
file |
diff |
annotate
|
| 2009-05-31 |
wenzelm |
discontinued support for Poly/ML 4.x versions;
|
file |
diff |
annotate
|
| 2009-05-30 |
wenzelm |
eliminated old Attrib.add_attributes (and Attrib.syntax);
|
file |
diff |
annotate
|