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;
wenzelm [Sat, 18 Jan 2014 19:24:45 +0100] rev 55034
tuned;
wenzelm [Sat, 18 Jan 2014 19:15:12 +0100] rev 55033
support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;
wenzelm [Fri, 17 Jan 2014 20:51:36 +0100] rev 55032
back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
wenzelm [Fri, 17 Jan 2014 20:36:57 +0100] rev 55031
tuned;
wenzelm [Fri, 17 Jan 2014 20:31:39 +0100] rev 55030
prefer user-space tool within Pure.thy;
wenzelm [Fri, 17 Jan 2014 20:20:20 +0100] rev 55029
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm [Fri, 17 Jan 2014 18:12:35 +0100] rev 55028
clarified Simplifier diagnostics -- simplified ML;
unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);