haftmann [Fri, 16 Jul 2010 13:58:37 +0200] rev 37843
merged
haftmann [Fri, 16 Jul 2010 13:58:29 +0200] rev 37842
a first sketch for Imperative HOL witht Scala
haftmann [Fri, 16 Jul 2010 13:57:46 +0200] rev 37841
don't fail gracefully
haftmann [Fri, 16 Jul 2010 13:57:29 +0200] rev 37840
restored long-broken syntax sanity checks
haftmann [Fri, 16 Jul 2010 13:57:29 +0200] rev 37839
tuned interpunctation
haftmann [Fri, 16 Jul 2010 10:23:21 +0200] rev 37838
fragments of Scala
haftmann [Thu, 15 Jul 2010 10:16:17 +0200] rev 37837
merged
haftmann [Thu, 15 Jul 2010 10:12:49 +0200] rev 37836
adjusted; fixed typo
haftmann [Thu, 15 Jul 2010 08:14:05 +0200] rev 37835
dropped spurious export_code
kleing [Wed, 14 Jul 2010 19:10:23 +0100] rev 37834
use different log server (macbroy23 down)
haftmann [Wed, 14 Jul 2010 17:27:54 +0200] rev 37833
more consistent spacing in generated monadic code
haftmann [Wed, 14 Jul 2010 17:16:02 +0200] rev 37832
braced needed in layout-insensitive syntax
haftmann [Wed, 14 Jul 2010 17:15:58 +0200] rev 37831
repaired some implementations of imperative operations
haftmann [Wed, 14 Jul 2010 16:45:30 +0200] rev 37830
repaired reference implementation for OCaml
haftmann [Wed, 14 Jul 2010 16:45:30 +0200] rev 37829
part of pervasive test
haftmann [Wed, 14 Jul 2010 16:45:30 +0200] rev 37828
avoid ambiguities; tuned
haftmann [Wed, 14 Jul 2010 16:45:29 +0200] rev 37827
repaired of_list implementation for SML, OCaml
haftmann [Wed, 14 Jul 2010 16:13:14 +0200] rev 37826
avoid export_code ... file -
haftmann [Wed, 14 Jul 2010 16:02:50 +0200] rev 37825
explicit optional checking
haftmann [Wed, 14 Jul 2010 15:49:29 +0200] rev 37824
added Isar syntax for code checking
haftmann [Wed, 14 Jul 2010 15:49:29 +0200] rev 37823
corrected import
haftmann [Wed, 14 Jul 2010 15:08:02 +0200] rev 37822
use generic description slot for formal code checking
haftmann [Wed, 14 Jul 2010 14:53:44 +0200] rev 37821
formal slot for code checker
haftmann [Wed, 14 Jul 2010 14:53:44 +0200] rev 37820
export_code without file prints to standard output
haftmann [Wed, 14 Jul 2010 14:20:47 +0200] rev 37819
check without explicit path
haftmann [Wed, 14 Jul 2010 14:16:12 +0200] rev 37818
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann [Wed, 14 Jul 2010 12:27:44 +0200] rev 37817
tuned infix syntax
haftmann [Wed, 14 Jul 2010 12:27:44 +0200] rev 37816
dropped M suffix; added predicate monad bind
haftmann [Wed, 14 Jul 2010 12:27:43 +0200] rev 37815
self-built symbol for part of bind operator
haftmann [Wed, 14 Jul 2010 09:42:44 +0200] rev 37814
redirect stderr to stdout
paulson [Tue, 13 Jul 2010 21:07:12 +0100] rev 37813
merged
paulson [Tue, 13 Jul 2010 11:27:19 +0100] rev 37812
merged
paulson [Tue, 13 Jul 2010 11:26:16 +0100] rev 37811
corrected mixfix declarations and tidied proofs
paulson [Tue, 13 Jul 2010 17:19:35 +0100] rev 37810
merged
paulson [Tue, 13 Jul 2010 17:19:08 +0100] rev 37809
Fixed syntax and tidied some proofs
bulwahn [Tue, 13 Jul 2010 18:01:42 +0200] rev 37808
correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
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
haftmann [Fri, 09 Jul 2010 08:11:10 +0200] rev 37751
nicer xsymbol syntax for fcomp and scomp
haftmann [Thu, 08 Jul 2010 17:23:05 +0200] rev 37750
dropped ancient in-place compilation of SML; more tests
haftmann [Thu, 08 Jul 2010 16:48:33 +0200] rev 37749
updated documentation
haftmann [Thu, 08 Jul 2010 16:41:57 +0200] rev 37748
dropped ancient in-place compilation of SML
haftmann [Thu, 08 Jul 2010 16:28:18 +0200] rev 37747
more accurate dependencies
haftmann [Thu, 08 Jul 2010 16:20:03 +0200] rev 37746
empty default
haftmann [Thu, 08 Jul 2010 16:19:24 +0200] rev 37745
checking generated code for various target languages
haftmann [Thu, 08 Jul 2010 16:19:24 +0200] rev 37744
tuned titles
haftmann [Thu, 08 Jul 2010 16:19:23 +0200] rev 37743
tuned module names
haftmann [Thu, 08 Jul 2010 16:17:44 +0200] rev 37742
tuned tabs
haftmann [Thu, 08 Jul 2010 16:17:44 +0200] rev 37741
tuned script
haftmann [Thu, 08 Jul 2010 09:36:23 +0200] rev 37740
combinator with_tmp_dir
haftmann [Thu, 08 Jul 2010 09:36:22 +0200] rev 37739
rm_tree: remove entire file system trees
berghofe [Wed, 07 Jul 2010 18:17:23 +0200] rev 37738
Boxes may now have different widths.
hoelzl [Wed, 07 Jul 2010 09:26:54 +0200] rev 37737
tuned
bulwahn [Wed, 07 Jul 2010 08:25:23 +0200] rev 37736
replaced manual derivation of equations for inductive predicates by automatic derivation by inductive_simps
bulwahn [Wed, 07 Jul 2010 08:25:22 +0200] rev 37735
added NEWS entry
bulwahn [Wed, 07 Jul 2010 08:25:21 +0200] rev 37734
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
huffman [Tue, 06 Jul 2010 08:08:35 -0700] rev 37733
merged
huffman [Mon, 05 Jul 2010 09:14:51 -0700] rev 37732
generalize type of is_interval to class euclidean_space
huffman [Mon, 05 Jul 2010 09:12:35 -0700] rev 37731
section -> subsection
huffman [Sun, 04 Jul 2010 09:26:30 -0700] rev 37730
generalize some lemmas about derivatives
huffman [Sun, 04 Jul 2010 09:25:17 -0700] rev 37729
uniqueness of Frechet derivative
wenzelm [Tue, 06 Jul 2010 21:33:14 +0200] rev 37728
implode pseudo utf8, i.e. decode byte-stuffed low ASCII characters;
wenzelm [Tue, 06 Jul 2010 10:02:24 +0200] rev 37727
merged
haftmann [Tue, 06 Jul 2010 09:27:49 +0200] rev 37726
even more fun with primrec
haftmann [Tue, 06 Jul 2010 09:21:15 +0200] rev 37725
refactored reference operations
haftmann [Tue, 06 Jul 2010 09:21:13 +0200] rev 37724
tuned