blanchet [Tue, 21 Jan 2014 13:05:22 +0100] rev 55094
removed dependency on 'Datatype' structure
blanchet [Tue, 21 Jan 2014 10:06:51 +0100] rev 55093
made SML/NJ happier
traytel [Tue, 21 Jan 2014 07:18:05 +0100] rev 55092
compile
blanchet [Tue, 21 Jan 2014 01:14:49 +0100] rev 55091
compile
blanchet [Mon, 20 Jan 2014 23:43:42 +0100] rev 55090
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
blanchet [Mon, 20 Jan 2014 23:34:26 +0100] rev 55089
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet [Mon, 20 Jan 2014 23:07:23 +0100] rev 55088
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
blanchet [Mon, 20 Jan 2014 22:24:48 +0100] rev 55087
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet [Mon, 20 Jan 2014 21:45:08 +0100] rev 55086
hide BNF notation
blanchet [Mon, 20 Jan 2014 21:32:41 +0100] rev 55085
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet [Mon, 20 Jan 2014 20:42:43 +0100] rev 55084
rationalized lemmas
blanchet [Mon, 20 Jan 2014 20:21:12 +0100] rev 55083
move BNF_LFP up the dependency chain
blanchet [Mon, 20 Jan 2014 20:00:33 +0100] rev 55082
compile
blanchet [Mon, 20 Jan 2014 19:53:10 +0100] rev 55081
updated docs
blanchet [Mon, 20 Jan 2014 19:51:56 +0100] rev 55080
have Nitpick lookup codatatypes
blanchet [Mon, 20 Jan 2014 19:05:25 +0100] rev 55079
removed dependency of BNF package on Nitpick
blanchet [Mon, 20 Jan 2014 18:59:53 +0100] rev 55078
deactivate one more cardinal notation
blanchet [Mon, 20 Jan 2014 18:25:44 +0100] rev 55077
fixed typo
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55076
compile
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55075
dissolved BNF session
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55074
rationalized dependencies
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55073
reduced dependencies + updated docs
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55072
minimized Nitpick's dependencies
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55071
moved BNF examples
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55070
rationalized dependencies
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55069
moved hide_const from BNF to Main
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55068
updated README
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55067
tuned names
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55066
tuning
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55065
compile
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55064
killed obsolete session
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55063
tuned comment
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55062
made BNF compile after move to HOL
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55061
adjusted comments
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55060
avoid nested 'Tools' directories
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55059
tuned comments
blanchet [Mon, 20 Jan 2014 18:24:56 +0100] rev 55058
moved BNF files to 'HOL'
blanchet [Mon, 20 Jan 2014 18:24:55 +0100] rev 55057
kill notations
blanchet [Mon, 20 Jan 2014 18:24:55 +0100] rev 55056
renamed '_FP' files to 'BNF_' files
blanchet [Mon, 20 Jan 2014 18:24:55 +0100] rev 55055
tuning
blanchet [Mon, 20 Jan 2014 18:24:55 +0100] rev 55054
moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
nipkow [Mon, 20 Jan 2014 16:14:19 +0100] rev 55053
tuned names
hoelzl [Mon, 20 Jan 2014 12:20:23 +0100] rev 55052
spelling
blanchet [Mon, 20 Jan 2014 10:07:07 +0100] rev 55051
killed obsolete provers from documentation
boehmes [Sun, 19 Jan 2014 23:02:00 +0100] rev 55050
merged
boehmes [Sun, 19 Jan 2014 22:38:17 +0100] rev 55049
removed obsolete remote_cvc3 and remote_z3
wenzelm [Sun, 19 Jan 2014 21:33:45 +0100] rev 55048
implicit "cartouche" method (experimental, undocumented);
wenzelm [Sun, 19 Jan 2014 21:00:42 +0100] rev 55047
more examples;
wenzelm [Sun, 19 Jan 2014 20:53:40 +0100] rev 55046
cartouche within antiquotation;
wenzelm [Sun, 19 Jan 2014 20:52:57 +0100] rev 55045
cartouche within nested args (attributes, methods, etc.);
wenzelm [Sun, 19 Jan 2014 20:39:48 +0100] rev 55044
group symbols;
haftmann [Sun, 19 Jan 2014 11:05:38 +0100] rev 55043
prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers
haftmann [Sun, 19 Jan 2014 11:05:37 +0100] rev 55042
table for code symbols
wenzelm [Sat, 18 Jan 2014 21:03:54 +0100] rev 55041
HTML output for \<newline>;
wenzelm [Sat, 18 Jan 2014 20:51:48 +0100] rev 55040
sorted entries according to components_checksum;
wenzelm [Sat, 18 Jan 2014 20:49:15 +0100] rev 55039
more unicode tokens;
diff -r ProofGeneral-4.2/isar/isar-unicode-tokens.el ProofGeneral-4.2-1/isar/isar-unicode-tokens.el
356c356,359
< ("some" "ϵ"))
---
> ("some" "ϵ")
> ("open" "‹")
> ("close" "›")
> ("newline" "⏎"))
wenzelm [Sat, 18 Jan 2014 20:20:56 +0100] rev 55038
prefer Isar commands over old-fashioned ML (see also a189c6274c7a);
removed pointless space: the second "_ \<Colon> _" should take precendence anyway;
wenzelm [Sat, 18 Jan 2014 19:46:58 +0100] rev 55037
crude latex macro for \<newline;
wenzelm [Sat, 18 Jan 2014 19:35:42 +0100] rev 55036
proper \<newline>;
wenzelm [Sat, 18 Jan 2014 19:31:32 +0100] rev 55035
unused;