haftmann [Tue, 13 Jul 2010 16:30:13 +0200] rev 37807
consolidated names of theorems
haftmann [Tue, 13 Jul 2010 16:21:49 +0200] rev 37806
qualified names for (really) all array operations
haftmann [Tue, 13 Jul 2010 16:12:40 +0200] rev 37805
canonical argument order for get
haftmann [Tue, 13 Jul 2010 16:00:56 +0200] rev 37804
qualified names for (almost) all array operations
haftmann [Tue, 13 Jul 2010 15:37:31 +0200] rev 37803
canonical argument order for present
haftmann [Tue, 13 Jul 2010 15:34:02 +0200] rev 37802
canonical argument order for length
kleing [Tue, 13 Jul 2010 11:23:21 +0100] rev 37801
merged
kleing [Tue, 13 Jul 2010 11:21:22 +0100] rev 37800
new crontab
haftmann [Tue, 13 Jul 2010 12:20:23 +0200] rev 37799
merged
haftmann [Tue, 13 Jul 2010 12:16:24 +0200] rev 37798
proper merge of operation changes and generic do-syntax
haftmann [Tue, 13 Jul 2010 12:05:20 +0200] rev 37797
merged
haftmann [Tue, 13 Jul 2010 12:01:34 +0200] rev 37796
hide_const; update replaces change
kleing [Tue, 13 Jul 2010 11:17:13 +0100] rev 37795
remove separate afp settings again, use plain mac-poly64-M4 instead.
kleing [Tue, 13 Jul 2010 11:01:12 +0100] rev 37794
merged
kleing [Tue, 13 Jul 2010 11:00:20 +0100] rev 37793
new settings for afp test
krauss [Tue, 13 Jul 2010 12:00:11 +0200] rev 37792
Heap_Monad uses Monad_Syntax
krauss [Tue, 13 Jul 2010 11:50:22 +0200] rev 37791
State_Monad uses Monad_Syntax
krauss [Tue, 13 Jul 2010 00:15:37 +0200] rev 37790
uniform do notation for monads
krauss [Tue, 13 Jul 2010 00:15:37 +0200] rev 37789
generic ad-hoc overloading via check/uncheck
haftmann [Tue, 13 Jul 2010 11:38:04 +0200] rev 37788
corrected title
haftmann [Tue, 13 Jul 2010 11:38:03 +0200] rev 37787
theorem collections do not contain default rules any longer
boehmes [Tue, 13 Jul 2010 02:29:05 +0200] rev 37786
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
added tests for Ball/Bex
wenzelm [Mon, 12 Jul 2010 22:35:41 +0200] rev 37785
removed unused/untested IOA 'automaton' package;
wenzelm [Mon, 12 Jul 2010 22:17:31 +0200] rev 37784
removed impractical tolerate_legacy_features flag;
wenzelm [Mon, 12 Jul 2010 22:14:11 +0200] rev 37783
tuned comment;
wenzelm [Mon, 12 Jul 2010 22:07:36 +0200] rev 37782
removed legacy aliases;
wenzelm [Mon, 12 Jul 2010 21:38:37 +0200] rev 37781
moved misc legacy stuff from OldGoals to Misc_Legacy;
OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
wenzelm [Mon, 12 Jul 2010 21:12:18 +0200] rev 37780
eliminated OldGoals.strip_context;
wenzelm [Mon, 12 Jul 2010 20:35:10 +0200] rev 37779
removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
wenzelm [Mon, 12 Jul 2010 20:21:39 +0200] rev 37778
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
use up-to-date ML_Compiler.exn_message;
wenzelm [Mon, 12 Jul 2010 18:59:38 +0200] rev 37777
some modernization of really ancient Meson experiments;
haftmann [Mon, 12 Jul 2010 16:40:48 +0200] rev 37776
dropped empty theory
haftmann [Mon, 12 Jul 2010 16:38:20 +0200] rev 37775
moved auxiliary lemma
haftmann [Mon, 12 Jul 2010 16:26:48 +0200] rev 37774
dropped unused lemmas of dubious value
haftmann [Mon, 12 Jul 2010 16:23:30 +0200] rev 37773
dropped unused lemmas of dubious value
haftmann [Mon, 12 Jul 2010 16:19:15 +0200] rev 37772
split off mrec into separate theory
haftmann [Mon, 12 Jul 2010 16:05:08 +0200] rev 37771
spelt out relational framework in a consistent way
haftmann [Mon, 12 Jul 2010 11:39:27 +0200] rev 37770
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
haftmann [Mon, 12 Jul 2010 11:21:56 +0200] rev 37769
merged
haftmann [Mon, 12 Jul 2010 11:21:27 +0200] rev 37768
moved co-regularity to class section; avoid duplicated class_deps
haftmann [Mon, 12 Jul 2010 10:48:37 +0200] rev 37767
dropped superfluous [code del]s
haftmann [Mon, 12 Jul 2010 08:58:27 +0200] rev 37766
merged
haftmann [Mon, 12 Jul 2010 08:58:13 +0200] rev 37765
dropped superfluous [code del]s
haftmann [Mon, 12 Jul 2010 08:58:12 +0200] rev 37764
more regular session structure
wenzelm [Sat, 10 Jul 2010 22:39:16 +0200] rev 37763
regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;
wenzelm [Sat, 10 Jul 2010 21:38:16 +0200] rev 37762
merged
kleing [Fri, 09 Jul 2010 16:44:05 +0100] rev 37761
Added current crontab of macbroy28
krauss [Fri, 09 Jul 2010 17:15:03 +0200] rev 37760
moved example to its own file in HOL/ex
haftmann [Fri, 09 Jul 2010 17:00:42 +0200] rev 37759
merged
haftmann [Fri, 09 Jul 2010 16:58:44 +0200] rev 37758
pervasive success combinator
krauss [Fri, 09 Jul 2010 16:32:25 +0200] rev 37757
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
haftmann [Fri, 09 Jul 2010 10:08:10 +0200] rev 37756
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann [Fri, 09 Jul 2010 09:48:54 +0200] rev 37755
adapted to changes
haftmann [Fri, 09 Jul 2010 09:48:53 +0200] rev 37754
guard combinator
haftmann [Fri, 09 Jul 2010 09:48:53 +0200] rev 37753
tuned reference theory
haftmann [Fri, 09 Jul 2010 09:48:52 +0200] rev 37752
tuned array theory