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);
2014-01-17 blanchet 2014-01-17 folded 'Wellfounded_More_FP' into 'Wellfounded'
2014-01-17 blanchet 2014-01-17 folded 'Order_Relation_More_FP' into 'Order_Relation'
2014-01-17 traytel 2014-01-17 support declaration of nonemptiness witnesses in bnf_decl
2014-01-16 blanchet 2014-01-16 hide short const name
2014-01-16 blanchet 2014-01-16 get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
2014-01-16 blanchet 2014-01-16 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
2014-01-16 blanchet 2014-01-16 compile (importing 'Metis' or 'Main' would have been an alternative)
2014-01-16 blanchet 2014-01-16 dissolved 'Fun_More_FP' (a BNF dependency)
2014-01-16 blanchet 2014-01-16 moved lemmas from 'Fun_More_FP' to where they belong
2014-01-16 blanchet 2014-01-16 moved 'Zorn' into 'Main', since it's a BNF dependency
2014-01-16 blanchet 2014-01-16 adapted to move of Wfrec