2014-05-16 noschinl 2014-05-16 added lemmas for -1
2014-05-16 blanchet 2014-05-16 proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
2014-05-16 nipkow 2014-05-16 new syntax for card, normalized spacing for #
2014-05-15 haftmann 2014-05-15 clarified stylized status of sandwich algebra
2014-05-15 haftmann 2014-05-15 dropped dead code
2014-05-15 haftmann 2014-05-15 accurate separation of static and dynamic context
2014-05-15 haftmann 2014-05-15 syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15 haftmann 2014-05-15 proper separation of static and dynamic context
2014-05-15 haftmann 2014-05-15 optimization for trivial cases
2014-05-15 haftmann 2014-05-15 modernized setup
2014-05-15 haftmann 2014-05-15 dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
2014-05-15 haftmann 2014-05-15 unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches
2014-05-15 haftmann 2014-05-15 normalize type variables of evaluation term by conversion
2014-05-15 blanchet 2014-05-15 more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
2014-05-15 blanchet 2014-05-15 new approach to silence proof methods, to avoid weird theory/context mismatches
2014-05-15 haftmann 2014-05-15 type
2014-05-14 wenzelm 2014-05-14 merged
2014-05-14 wenzelm 2014-05-14 restrict default docking layout to bare minimum -- NB: Simplifier Trace still needs fine-tuning to show up on demand;
2014-05-14 wenzelm 2014-05-14 updated isatest;
2014-05-14 wenzelm 2014-05-14 updated to polyml-5.5.2;
2014-05-14 wenzelm 2014-05-14 practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
2014-05-14 wenzelm 2014-05-14 updated to polyml-5.5.2;
2014-05-14 desharna 2014-05-14 document 'set_empty'
2014-05-12 desharna 2014-05-12 generate 'set_empty' theorem for BNFs
2014-05-08 desharna 2014-05-08 document 'map_id0'
2014-05-08 desharna 2014-05-08 note map_id0 more often
2014-05-14 nipkow 2014-05-14 added lemma
2014-05-13 nipkow 2014-05-13 added lemmas
2014-05-13 blanchet 2014-05-13 transfer theorems since 'silence_methods' may change the theory
2014-05-13 hoelzl 2014-05-13 add mono rules for diff
2014-05-13 hoelzl 2014-05-13 clean up Lebesgue integration
2014-05-13 blanchet 2014-05-13 more bnf_decl -> bnf_axiomatization
2014-05-13 blanchet 2014-05-13 tuned docs
2014-05-13 blanchet 2014-05-13 hide more internal names
2014-05-13 blanchet 2014-05-13 tuning
2014-05-13 wenzelm 2014-05-13 no reset for 'end' -- e.g. relevant for 'notepad';
2014-05-13 traytel 2014-05-13 updated keywords
2014-05-13 traytel 2014-05-13 bnf_decl -> bnf_axiomatization
2014-05-12 wenzelm 2014-05-12 tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
2014-05-12 webertj 2014-05-12 Replaced refute with nitpick.
2014-05-12 wenzelm 2014-05-12 NEWS;
2014-05-12 wenzelm 2014-05-12 tuned message;
2014-05-12 wenzelm 2014-05-12 smarter recovery from toplevel type error;
2014-05-11 wenzelm 2014-05-11 more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion; prefer JDialog for FloatingWindowContainer, to keep it in front of the main window; updated to Navigator.jar 2.5, SideKick.jar 1.6;
2014-05-09 wenzelm 2014-05-09 updated keywords;
2014-05-09 wenzelm 2014-05-09 merged
2014-05-09 wenzelm 2014-05-09 more markup;
2014-05-09 wenzelm 2014-05-09 more position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-09 wenzelm 2014-05-09 always bounce focus back to main text area, unless explicit focus component is given here (see also 7b65f4da136d);
2014-05-09 wenzelm 2014-05-09 tuned signature;
2014-05-09 haftmann 2014-05-09 delete attribute for code abbrev
2014-05-09 haftmann 2014-05-09 dropped term_of obfuscation -- not really required; tuned theory structure
2014-05-09 haftmann 2014-05-09 hardcoded nbe and sml into value command
2014-05-09 haftmann 2014-05-09 modernized setups
2014-05-09 haftmann 2014-05-09 degeneralized value command into HOL
2014-05-09 haftmann 2014-05-09 dimiss simplified as evaluator due to little practical relevance
2014-05-09 haftmann 2014-05-09 prefer separate command for approximation
2014-05-09 haftmann 2014-05-09 removed junk from library theory
2014-05-09 haftmann 2014-05-09 note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs
2014-05-09 haftmann 2014-05-09 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;