| 2010-03-20 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| 2010-03-17 |
huffman |
NEWS: Nat_Bijection library
|
file |
diff |
annotate
|
| 2010-03-13 |
wenzelm |
local theory specifications handle hidden polymorphism implicitly;
|
file |
diff |
annotate
|
| 2010-03-13 |
wenzelm |
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
|
file |
diff |
annotate
|
| 2010-03-13 |
wenzelm |
command 'typedef' now works within a local theory context;
|
file |
diff |
annotate
|
| 2010-03-11 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2010-03-11 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| 2010-03-09 |
wenzelm |
localized typedecl;
|
file |
diff |
annotate
|
| 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
|