| 2009-12-11 |
wenzelm |
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
|
file |
diff |
annotate
|
| 2009-12-11 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2009-12-05 |
haftmann |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file |
diff |
annotate
|
| 2009-12-04 |
haftmann |
merged, resolving minor conflicts
|
file |
diff |
annotate
|
| 2009-12-04 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2009-12-04 |
wenzelm |
back to after-release mode;
|
file |
diff |
annotate
|
| 2009-11-23 |
wenzelm |
more tuning for release;
|
file |
diff |
annotate
|
| 2009-11-23 |
haftmann |
tuned NEWS
|
file |
diff |
annotate
|
| 2009-11-22 |
haftmann |
more uniform view on various number theory refinement steps
|
file |
diff |
annotate
|
| 2009-11-22 |
wenzelm |
more NEWS, more tuning for release;
|
file |
diff |
annotate
|
| 2009-11-22 |
wenzelm |
misc tuning and updates for official release;
|
file |
diff |
annotate
|
| 2009-11-21 |
kleing |
wwwfind support currently for Linux only
|
file |
diff |
annotate
|
| 2009-11-20 |
huffman |
NEWS: HOLCF changes since the last release
|
file |
diff |
annotate
|
| 2009-11-20 |
kleing |
added NEWS item for wwwfind
|
file |
diff |
annotate
|
| 2009-11-19 |
hoelzl |
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
|
file |
diff |
annotate
|
| 2009-11-13 |
nipkow |
-
|
file |
diff |
annotate
|
| 2009-11-12 |
bulwahn |
added a tabled implementation of the reflexive transitive closure
|
file |
diff |
annotate
|
| 2009-11-12 |
hoelzl |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
file |
diff |
annotate
|
| 2009-11-12 |
bulwahn |
announcing the predicate compiler in NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2009-11-08 |
wenzelm |
updated functor Theory_Data, Proof_Data, Generic_Data;
|
file |
diff |
annotate
|
| 2009-11-06 |
boehmes |
added documentation for local SMT solver setup and available SMT options,
|
file |
diff |
annotate
|
| 2009-11-06 |
krauss |
renamed method induct_scheme to induction_schema
|
file |
diff |
annotate
|
| 2009-11-06 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2009-11-03 |
boehmes |
added HOL-Boogie
|
file |
diff |
annotate
|
| 2009-10-30 |
haftmann |
combined former theories Divides and IntDiv to one theory Divides
|
file |
diff |
annotate
|
| 2009-10-28 |
paulson |
Probability tweaks
|
file |
diff |
annotate
|
| 2009-10-28 |
paulson |
New theory Probability, which contains a development of measure theory
|
file |
diff |
annotate
|
| 2009-10-27 |
paulson |
merged
|
file |
diff |
annotate
|
| 2009-10-27 |
paulson |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
file |
diff |
annotate
|
| 2009-10-26 |
blanchet |
merged
|
file |
diff |
annotate
|
| 2009-10-22 |
blanchet |
added Nitpick's theory and ML files to Isabelle/HOL;
|
file |
diff |
annotate
|
| 2009-10-23 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
| 2009-10-22 |
nipkow |
inv_onto -> inv_into
|
file |
diff |
annotate
|
| 2009-10-20 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| 2009-10-20 |
boehmes |
added proof reconstructon for Z3,
|
file |
diff |
annotate
|
| 2009-10-18 |
nipkow |
certificates for sos
|
file |
diff |
annotate
|
| 2009-10-18 |
nipkow |
merged
|
file |
diff |
annotate
|
| 2009-10-18 |
nipkow |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
file |
diff |
annotate
|
| 2009-10-17 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| 2009-10-17 |
ballarin |
Finished revisions of locales tutorial.
|
file |
diff |
annotate
|
| 2009-10-17 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
| 2009-10-09 |
haftmann |
term styles also cover antiquotations term_type and typeof
|
file |
diff |
annotate
|
| 2009-10-08 |
haftmann |
new generalized concept for term styles
|
file |
diff |
annotate
|
| 2009-10-01 |
ballarin |
News entry: inheritance of mixins; print_interps.
|
file |
diff |
annotate
|
| 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
|