| 2010-04-19 |
wenzelm |
polyml-platform script is superseded by ISABELLE_PLATFORM;
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
|
file |
diff |
annotate
|
| 2010-04-15 |
haftmann |
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
|
file |
diff |
annotate
|
| 2010-04-07 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
| 2010-02-15 |
ballarin |
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
|
file |
diff |
annotate
|
| 2010-03-30 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2010-03-28 |
wenzelm |
configuration options admit dynamic default values;
|
file |
diff |
annotate
|
| 2010-03-27 |
boehmes |
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
|
file |
diff |
annotate
|
| 2010-03-26 |
boehmes |
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
|
file |
diff |
annotate
|
| 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
|