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
2014-01-16 blanchet 2014-01-16 moved Wfrec to Main, since it is a dependency of cardinals, hence BNFs
2014-01-15 wenzelm 2014-01-15 added \<newline> symbol, which is used for char/string literals in HOL;
2014-01-15 wenzelm 2014-01-15 general notion of auxiliary bounds within context; revert_bounds as part of regular unparse_term; avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);
2014-01-15 wenzelm 2014-01-15 merged
2014-01-15 wenzelm 2014-01-15 fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;
2014-01-15 nipkow 2014-01-15 tuned text
2014-01-15 nipkow 2014-01-15 tuned
2014-01-14 blanchet 2014-01-14 automatically solve proof obligations produced for code equations
2014-01-14 blanchet 2014-01-14 use 'disc_exhausts' property both from types on which 'case's take place and on return type
2014-01-13 wenzelm 2014-01-13 activation of Z3 via "z3_non_commercial" system option (without requiring restart);
2014-01-13 wenzelm 2014-01-13 tuned;
2014-01-13 blanchet 2014-01-13 use the right context in 'unfold_thms id_def'
2014-01-13 blanchet 2014-01-13 repaired 'ctr' tactic w.r.t. 'split'
2014-01-13 nipkow 2014-01-13 tuned
2014-01-12 wenzelm 2014-01-12 merged
2014-01-12 wenzelm 2014-01-12 NEWS;
2014-01-12 wenzelm 2014-01-12 proper context for clear_simpset: preserve dounds, depth; dismantled obsolete debug_bounds/check_bounds;
2014-01-12 wenzelm 2014-01-12 clarified context;