krauss [Tue, 07 Nov 2006 22:06:32 +0100] rev 21237
untabified
wenzelm [Tue, 07 Nov 2006 21:30:03 +0100] rev 21236
complex goal statements: misc cleanup;
krauss [Tue, 07 Nov 2006 21:28:14 +0100] rev 21235
Added datatype hook to declare all case_congs as "fundef_cong" automatically.
wenzelm [Tue, 07 Nov 2006 19:40:56 +0100] rev 21234
removed obsolete theorem statements (cf. specification.ML);
wenzelm [Tue, 07 Nov 2006 19:40:13 +0100] rev 21233
tuned specifications;
wenzelm [Tue, 07 Nov 2006 19:39:54 +0100] rev 21232
fixed locale fact references;
wenzelm [Tue, 07 Nov 2006 19:39:53 +0100] rev 21231
removed obsolete print_state_hook;
wenzelm [Tue, 07 Nov 2006 19:39:52 +0100] rev 21230
theorem statements: incorporate Obtain.statement, tuned;
wenzelm [Tue, 07 Nov 2006 19:39:50 +0100] rev 21229
moved statement to specification.ML;
wenzelm [Tue, 07 Nov 2006 19:39:48 +0100] rev 21228
removed obsolete Locale.smart_theorem;
wenzelm [Tue, 07 Nov 2006 19:39:46 +0100] rev 21227
avoid handling of arbitrary exceptions;
schirmer [Tue, 07 Nov 2006 18:25:48 +0100] rev 21226
field-update in records is generalised to take a function on the field
rather than the new value.
schirmer [Tue, 07 Nov 2006 18:14:53 +0100] rev 21225
exported intro_locales_tac
----------------------------------------------------------------------
paulson [Tue, 07 Nov 2006 16:21:54 +0100] rev 21224
Proper theorem names at last, no fakes!!
Added set_prover function to set various parameters to improve success rate.
Fixed the auto settings for E.
haftmann [Tue, 07 Nov 2006 15:07:02 +0100] rev 21223
some corrections
haftmann [Tue, 07 Nov 2006 14:49:09 +0100] rev 21222
adjusted title
wenzelm [Tue, 07 Nov 2006 14:30:03 +0100] rev 21221
simplified dest_eq;
do not export debuging stuff;
has_tvars: actually check all types within a term, not just its resulting type;
tuned;
wenzelm [Tue, 07 Nov 2006 14:30:00 +0100] rev 21220
commented out parts which have been inactive (unintentionally) for a long time;
wenzelm [Tue, 07 Nov 2006 14:29:58 +0100] rev 21219
removed obsolete dest_eq_typ;
wenzelm [Tue, 07 Nov 2006 14:29:57 +0100] rev 21218
tuned hypsubst setup;
haftmann [Tue, 07 Nov 2006 14:14:36 +0100] rev 21217
continued
haftmann [Tue, 07 Nov 2006 14:03:06 +0100] rev 21216
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann [Tue, 07 Nov 2006 14:03:04 +0100] rev 21215
made locale partial_order compatible with axclass order
haftmann [Tue, 07 Nov 2006 14:02:10 +0100] rev 21214
adjusted two lemma names due to name change in interpretation
haftmann [Tue, 07 Nov 2006 14:02:08 +0100] rev 21213
changed import order
krauss [Tue, 07 Nov 2006 12:20:11 +0100] rev 21212
Added a (stub of a) function tutorial
krauss [Tue, 07 Nov 2006 11:53:55 +0100] rev 21211
Preparations for making "lexicographic_order" part of "fun"
wenzelm [Tue, 07 Nov 2006 11:47:57 +0100] rev 21210
renamed 'const_syntax' to 'notation';
wenzelm [Tue, 07 Nov 2006 11:47:56 +0100] rev 21209
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm [Tue, 07 Nov 2006 11:46:50 +0100] rev 21208
replaced const_syntax by notation, which operates on terms;
read_const: include type;
wenzelm [Tue, 07 Nov 2006 11:46:49 +0100] rev 21207
Isar.context: proper error;
wenzelm [Tue, 07 Nov 2006 11:46:48 +0100] rev 21206
replaced const_syntax by notation, which operates on terms;
wenzelm [Tue, 07 Nov 2006 11:46:47 +0100] rev 21205
read_const: include type;
wenzelm [Tue, 07 Nov 2006 11:46:46 +0100] rev 21204
renamed 'const_syntax' to 'notation';
proper notation for fixed variables;
wenzelm [Tue, 07 Nov 2006 11:46:45 +0100] rev 21203
updated;
berghofe [Tue, 07 Nov 2006 11:28:25 +0100] rev 21202
Adapted to changes in FixedPoint theory.
krauss [Tue, 07 Nov 2006 09:59:43 +0100] rev 21201
method exported
krauss [Tue, 07 Nov 2006 09:41:14 +0100] rev 21200
updated NEWS
krauss [Tue, 07 Nov 2006 09:33:47 +0100] rev 21199
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
Richer structures do not inherit from semiring_0 anymore, because
anihilation is a theorem there, not an axiom.
* Generalized axclass "recpower" to arbitrary monoid, not just
commutative semirings.
haftmann [Tue, 07 Nov 2006 08:03:46 +0100] rev 21198
added gfx
haftmann [Mon, 06 Nov 2006 16:29:21 +0100] rev 21197
dropped blastdata.ML
haftmann [Mon, 06 Nov 2006 16:28:37 +0100] rev 21196
(adjustions)
haftmann [Mon, 06 Nov 2006 16:28:36 +0100] rev 21195
two further lemmas on split
haftmann [Mon, 06 Nov 2006 16:28:35 +0100] rev 21194
removed dependency of ord on eq
haftmann [Mon, 06 Nov 2006 16:28:34 +0100] rev 21193
removed itrev as inlining theorem
haftmann [Mon, 06 Nov 2006 16:28:33 +0100] rev 21192
added state monad to HOL library
haftmann [Mon, 06 Nov 2006 16:28:31 +0100] rev 21191
code generator module naming improved
haftmann [Mon, 06 Nov 2006 16:28:30 +0100] rev 21190
(continued)
haftmann [Mon, 06 Nov 2006 16:28:29 +0100] rev 21189
(continued)
krauss [Mon, 06 Nov 2006 12:04:44 +0100] rev 21188
minor cleanup
wenzelm [Sun, 05 Nov 2006 21:44:42 +0100] rev 21187
case_tr: do not intern already internal consts;
wenzelm [Sun, 05 Nov 2006 21:44:41 +0100] rev 21186
updated;
wenzelm [Sun, 05 Nov 2006 21:44:40 +0100] rev 21185
removed isactrlconst;
wenzelm [Sun, 05 Nov 2006 21:44:39 +0100] rev 21184
instantiate: avoid global references;
wenzelm [Sun, 05 Nov 2006 21:44:37 +0100] rev 21183
added const_syntax_name;
wenzelm [Sun, 05 Nov 2006 21:44:35 +0100] rev 21182
removed obsolete first_duplicate;