wenzelm [Sun, 08 Mar 2009 00:16:34 +0100] rev 30354
merged
haftmann [Sat, 07 Mar 2009 23:41:04 +0100] rev 30353
merged
haftmann [Sat, 07 Mar 2009 15:20:32 +0100] rev 30352
restructured theory Set.thy
wenzelm [Sat, 07 Mar 2009 23:37:09 +0100] rev 30351
merged
blanchet [Sat, 07 Mar 2009 17:05:40 +0100] rev 30350
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
blanchet [Sat, 07 Mar 2009 16:47:36 +0100] rev 30349
Added a second timeout mechanism to Refute.
For some reason, TimeLimit.timeLimit often does not work, and it
leaves Refute running forever, making any evaluation using
Mutabelle or Mirabelle impossible. The redundant timeout seems to
do the trick.
blanchet [Sat, 07 Mar 2009 12:27:26 +0100] rev 30348
merged
blanchet [Sat, 07 Mar 2009 12:26:56 +0100] rev 30347
Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
wenzelm [Sat, 07 Mar 2009 23:30:58 +0100] rev 30346
minimal adaptions for abstract binding type;
wenzelm [Sat, 07 Mar 2009 22:17:25 +0100] rev 30345
more uniform handling of binding in packages;
wenzelm [Sat, 07 Mar 2009 22:16:50 +0100] rev 30344
more uniform handling of binding in targets and derived elements;
wenzelm [Sat, 07 Mar 2009 22:12:07 +0100] rev 30343
replace old bstring by binding for logical primitives: class, type, const etc.;
wenzelm [Sat, 07 Mar 2009 22:04:59 +0100] rev 30342
moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;
wenzelm [Sat, 07 Mar 2009 21:57:36 +0100] rev 30341
adapted Syntax.const_name;
wenzelm [Sat, 07 Mar 2009 21:20:17 +0100] rev 30340
canonical argument order for type_name, const_name;
wenzelm [Sat, 07 Mar 2009 21:19:24 +0100] rev 30339
added const_binding;
wenzelm [Sat, 07 Mar 2009 21:18:37 +0100] rev 30338
added prefix_name, suffix_name;
added eq_name;
added opaque signature constraint to prevent accidental equality test;
wenzelm [Sat, 07 Mar 2009 12:07:30 +0100] rev 30337
Theory.add_axioms/add_defs: replaced old bstring by binding;
wenzelm [Sat, 07 Mar 2009 11:45:56 +0100] rev 30336
renamed rep_ss to MetaSimplifier.internal_ss;
wenzelm [Sat, 07 Mar 2009 11:32:31 +0100] rev 30335
Binding.str_of: removed verbose feature, include qualifier in output;
renamed Binding.add_prefix to Binding.prefix;
wenzelm [Sat, 07 Mar 2009 11:31:41 +0100] rev 30334
oracle: proper name position, tuned;
haftmann [Sat, 07 Mar 2009 10:06:58 +0100] rev 30333
merged
haftmann [Sat, 07 Mar 2009 10:06:31 +0100] rev 30332
drop poisonous code equations
haftmann [Sat, 07 Mar 2009 10:06:12 +0100] rev 30331
suppress document output
haftmann [Fri, 06 Mar 2009 20:30:19 +0100] rev 30330
theory with syntax for lattice operations
haftmann [Fri, 06 Mar 2009 20:30:18 +0100] rev 30329
added babel -- necessary for bind infix syntax
haftmann [Fri, 06 Mar 2009 20:30:17 +0100] rev 30328
added enumeration of predicates
haftmann [Fri, 06 Mar 2009 20:30:17 +0100] rev 30327
moved instance option :: finite to Option.thy
haftmann [Fri, 06 Mar 2009 20:30:16 +0100] rev 30326
constructive version of Cantor's first diagonalization argument
haftmann [Fri, 06 Mar 2009 20:29:37 +0100] rev 30325
equalities for Min, Max
wenzelm [Fri, 06 Mar 2009 23:25:08 +0100] rev 30324
merged
nipkow [Fri, 06 Mar 2009 22:06:33 +0100] rev 30323
added lemma
nipkow [Fri, 06 Mar 2009 21:57:56 +0100] rev 30322
merged
nipkow [Fri, 06 Mar 2009 21:57:46 +0100] rev 30321
Docs
wenzelm [Fri, 06 Mar 2009 22:50:30 +0100] rev 30320
eliminated Output.immediate_output -- violates the official message channel protocol;
wenzelm [Fri, 06 Mar 2009 22:47:32 +0100] rev 30319
schedule_seq: handle after_load errors as in schedule_futures;
wenzelm [Fri, 06 Mar 2009 22:32:27 +0100] rev 30318
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm [Fri, 06 Mar 2009 21:49:58 +0100] rev 30317
improved error handling for document antiquotations;
blanchet [Fri, 06 Mar 2009 19:38:03 +0100] rev 30316
merged
nipkow [Fri, 06 Mar 2009 17:39:05 +0100] rev 30315
merged
blanchet [Fri, 06 Mar 2009 19:37:31 +0100] rev 30314
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
Also replaced calls to "Output.immediate_output" with "priority" or "tracing", because "immediate_output" causes some problems (as explained by Makarius to Sascha).
nipkow [Fri, 06 Mar 2009 17:38:47 +0100] rev 30313
added lemmas
blanchet [Fri, 06 Mar 2009 17:21:17 +0100] rev 30312
Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead.
I tested the affected symbols (card, finite, lfp, and gfp), and Refute now works better than before (i.e., more precision and more speed).
blanchet [Fri, 06 Mar 2009 15:54:33 +0100] rev 30311
merged
blanchet [Fri, 06 Mar 2009 15:31:26 +0100] rev 30310
merged
blanchet [Fri, 06 Mar 2009 15:31:07 +0100] rev 30309
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
haftmann [Fri, 06 Mar 2009 15:51:18 +0100] rev 30308
merged
haftmann [Fri, 06 Mar 2009 11:10:57 +0100] rev 30307
merged
haftmann [Fri, 06 Mar 2009 11:10:18 +0100] rev 30306
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann [Thu, 05 Mar 2009 08:24:28 +0100] rev 30305
merged
haftmann [Thu, 05 Mar 2009 08:23:11 +0100] rev 30304
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann [Thu, 05 Mar 2009 08:23:10 +0100] rev 30303
tuned
haftmann [Thu, 05 Mar 2009 08:23:09 +0100] rev 30302
moved complete_lattice to Set.thy
haftmann [Thu, 05 Mar 2009 08:23:08 +0100] rev 30301
dropped Id
haftmann [Fri, 06 Mar 2009 14:51:18 +0100] rev 30300
corrected slip in NEWS
haftmann [Fri, 06 Mar 2009 14:33:42 +0100] rev 30299
merged