2015-09-29 wenzelm 2015-09-29 clarified modules;
2015-09-27 haftmann 2015-09-27 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-09-27 haftmann 2015-09-27 more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
2015-09-28 hoelzl 2015-09-28 Caratheodory: cleanup and modernisation
2015-09-25 traytel 2015-09-25 restructure fresh variable generation to make exports more wellformed
2015-09-25 traytel 2015-09-25 more canonical context threading
2015-09-25 wenzelm 2015-09-25 merged
2015-09-25 wenzelm 2015-09-25 documentation for "Semantic subtype definitions"; misc tuning and simplification;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-25 wenzelm 2015-09-25 less redundant output;
2015-09-25 wenzelm 2015-09-25 proper context;
2015-09-25 wenzelm 2015-09-25 tuned;
2015-09-25 wenzelm 2015-09-25 tuned;
2015-09-25 wenzelm 2015-09-25 tuned;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-09-23 wenzelm 2015-09-23 tuned signature;
2015-09-23 wenzelm 2015-09-23 tuned output;
2015-09-23 wenzelm 2015-09-23 tuned output;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned output;
2015-09-22 wenzelm 2015-09-22 separate command 'print_definitions';
2015-09-22 wenzelm 2015-09-22 tuned;
2015-09-22 wenzelm 2015-09-22 clarified deps entry: global names for arguments;
2015-09-22 wenzelm 2015-09-22 renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned whitespace;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-09-25 hoelzl 2015-09-25 prove Liminf_inverse_ereal
2015-09-24 immler 2015-09-24 merged
2015-09-24 immler 2015-09-24 exchange uniform limit and integral
2015-09-24 traytel 2015-09-24 congruence rules for the relator
2015-09-24 traytel 2015-09-24 conceal only the definitional theorems of map, set, rel (and not the actual constants)
2015-09-24 traytel 2015-09-24 more useful properties of the relators
2015-09-24 traytel 2015-09-24 tuned proofs (less warnings)
2015-09-23 paulson 2015-09-23 Useful facts about min/max, etc.
2015-09-23 paulson 2015-09-23 Merge
2015-09-23 paulson 2015-09-23 fixed a VERY SLOW proof
2015-09-22 paulson 2015-09-22 SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
2015-09-22 paulson 2015-09-22 New lemmas
2015-09-22 paulson 2015-09-22 Prepared two non-terminating proofs; no obvious link with my changes
2015-09-23 nipkow 2015-09-23 added AVL and lookup function
2015-09-23 nipkow 2015-09-23 tuned
2015-09-22 nipkow 2015-09-22 merged
2015-09-22 nipkow 2015-09-22 unified isin-proofs
2015-09-22 haftmann 2015-09-22 tuned
2015-09-22 haftmann 2015-09-22 include some data structures into code generation
2015-09-22 haftmann 2015-09-22 effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
2015-09-22 nipkow 2015-09-22 tuned references
2015-09-22 nipkow 2015-09-22 added red black trees
2015-09-21 wenzelm 2015-09-21 clarified markup; tuned signature;
2015-09-21 wenzelm 2015-09-21 isabelle update_cartouches;
2015-09-21 wenzelm 2015-09-21 merged
2015-09-21 wenzelm 2015-09-21 tuned GUI;
2015-09-21 wenzelm 2015-09-21 removed auto update -- bad reactivity;
2015-09-21 wenzelm 2015-09-21 clarified isabelle.update-state;
2015-09-21 wenzelm 2015-09-21 more reactive update, like Output panel;