| 2010-03-06 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
| 2010-03-03 |
wenzelm |
authentic syntax for *all* logical entities;
|
file |
diff |
annotate
|
| 2010-03-01 |
wenzelm |
added type_notation command;
|
file |
diff |
annotate
|
| 2010-02-27 |
wenzelm |
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
|
file |
diff |
annotate
|
| 2010-02-27 |
wenzelm |
ML antiquotations for type classes;
|
file |
diff |
annotate
|
| 2010-02-26 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-02-24 |
haftmann |
renamed theory Rational to Rat
|
file |
diff |
annotate
|
| 2010-02-25 |
wenzelm |
more orthogonal antiquotations for type constructors;
|
file |
diff |
annotate
|
| 2010-02-24 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| 2010-02-22 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-02-22 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-02-22 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-02-22 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-02-19 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-02-19 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-02-21 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2010-02-21 |
wenzelm |
NEWS: authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
| 2010-02-15 |
wenzelm |
renamed InfixName to Infix etc.;
|
file |
diff |
annotate
|
| 2010-02-15 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
| 2010-02-11 |
wenzelm |
added ML antiquotation @{syntax_const};
|
file |
diff |
annotate
|
| 2010-02-10 |
wenzelm |
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-02-10 |
haftmann |
moved constants inverse and divide to Ring.thy
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
NEWS: ax_simps
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2010-02-08 |
haftmann |
separate theory for index structures
|
file |
diff |
annotate
|
| 2010-02-05 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| 2010-02-07 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| 2010-02-06 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 2010-01-28 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| 2010-01-22 |
haftmann |
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
|
file |
diff |
annotate
|
| 2010-01-22 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-01-19 |
hoelzl |
Add transpose to the List-theory.
|
file |
diff |
annotate
|
| 2010-01-04 |
wenzelm |
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
|
file |
diff |
annotate
|
| 2010-01-04 |
wenzelm |
discontinued old ISABELLE and ISATOOL environment settings;
|
file |
diff |
annotate
|
| 2010-01-04 |
wenzelm |
discontinued special HOL_USEDIR_OPTIONS;
|
file |
diff |
annotate
|
| 2009-12-23 |
haftmann |
reduced code generator cache to the baremost minimum; corrected spelling
|
file |
diff |
annotate
|
| 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
|