2014-01-20 blanchet 2014-01-20 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
2014-01-20 blanchet 2014-01-20 hide BNF notation
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2014-01-20 blanchet 2014-01-20 rationalized lemmas
2014-01-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2014-01-20 blanchet 2014-01-20 compile
2014-01-20 blanchet 2014-01-20 updated docs
2014-01-20 blanchet 2014-01-20 have Nitpick lookup codatatypes
2014-01-20 blanchet 2014-01-20 removed dependency of BNF package on Nitpick
2014-01-20 blanchet 2014-01-20 deactivate one more cardinal notation
2014-01-20 blanchet 2014-01-20 fixed typo
2014-01-20 blanchet 2014-01-20 compile
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-20 blanchet 2014-01-20 rationalized dependencies
2014-01-20 blanchet 2014-01-20 reduced dependencies + updated docs
2014-01-20 blanchet 2014-01-20 minimized Nitpick's dependencies
2014-01-20 blanchet 2014-01-20 moved BNF examples
2014-01-20 blanchet 2014-01-20 rationalized dependencies
2014-01-20 blanchet 2014-01-20 moved hide_const from BNF to Main
2014-01-20 blanchet 2014-01-20 updated README
2014-01-20 blanchet 2014-01-20 tuned names
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 compile
2014-01-20 blanchet 2014-01-20 killed obsolete session
2014-01-20 blanchet 2014-01-20 tuned comment
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories
2014-01-20 blanchet 2014-01-20 tuned comments
2014-01-20 blanchet 2014-01-20 moved BNF files to 'HOL'
2014-01-20 blanchet 2014-01-20 kill notations
2014-01-20 blanchet 2014-01-20 renamed '_FP' files to 'BNF_' files
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
2014-01-20 nipkow 2014-01-20 tuned names
2014-01-20 hoelzl 2014-01-20 spelling
2014-01-20 blanchet 2014-01-20 killed obsolete provers from documentation
2014-01-19 boehmes 2014-01-19 merged
2014-01-19 boehmes 2014-01-19 removed obsolete remote_cvc3 and remote_z3
2014-01-19 wenzelm 2014-01-19 implicit "cartouche" method (experimental, undocumented);
2014-01-19 wenzelm 2014-01-19 more examples;
2014-01-19 wenzelm 2014-01-19 cartouche within antiquotation;
2014-01-19 wenzelm 2014-01-19 cartouche within nested args (attributes, methods, etc.);
2014-01-19 wenzelm 2014-01-19 group symbols;
2014-01-19 haftmann 2014-01-19 prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers
2014-01-19 haftmann 2014-01-19 table for code symbols
2014-01-18 wenzelm 2014-01-18 HTML output for \<newline>;
2014-01-18 wenzelm 2014-01-18 sorted entries according to components_checksum;
2014-01-18 wenzelm 2014-01-18 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" "⏎"))
2014-01-18 wenzelm 2014-01-18 prefer Isar commands over old-fashioned ML (see also a189c6274c7a); removed pointless space: the second "_ \<Colon> _" should take precendence anyway;
2014-01-18 wenzelm 2014-01-18 crude latex macro for \<newline;
2014-01-18 wenzelm 2014-01-18 proper \<newline>;
2014-01-18 wenzelm 2014-01-18 unused;
2014-01-18 wenzelm 2014-01-18 tuned;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2014-01-17 wenzelm 2014-01-17 back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
2014-01-17 wenzelm 2014-01-17 tuned;
2014-01-17 wenzelm 2014-01-17 prefer user-space tool within Pure.thy;
2014-01-17 wenzelm 2014-01-17 clarified @{rail} syntax: prefer explicit \<newline> symbol;
2014-01-17 wenzelm 2014-01-17 clarified Simplifier diagnostics -- simplified ML; unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);