2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 tuned message;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 avoid hard-wired theory names;
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-21 wenzelm 2014-03-21 added splash screen for jvm boot, which is important for initial encounter to avoid multiple copies running against each other;
2014-03-21 wenzelm 2014-03-21 merged
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 tuned;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-21 paulson 2014-03-21 a few new lemmas and generalisations of old ones
2014-03-21 traytel 2014-03-21 simplified internal datatype construction
2014-03-20 wenzelm 2014-03-20 merged
2014-03-20 wenzelm 2014-03-20 merged
2014-03-20 wenzelm 2014-03-20 produce qualified names more directly;
2014-03-20 wenzelm 2014-03-20 more symbols;
2014-03-20 wenzelm 2014-03-20 more static checking of proof methods;
2014-03-20 wenzelm 2014-03-20 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
2014-03-20 wenzelm 2014-03-20 more standard method_setup; enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range;
2014-03-20 wenzelm 2014-03-20 tuned error, according to "use" in General/secure.ML;
2014-03-20 wenzelm 2014-03-20 tuned proofs;
2014-03-20 huffman 2014-03-20 generalize more theorems
2014-03-20 huffman 2014-03-20 generalize some theorems
2014-03-20 paulson 2014-03-20 fixing messy proofs
2014-03-20 kleing 2014-03-20 pointer to the other proof direction
2014-03-19 huffman 2014-03-19 generalize theory of operator norms to work with class real_normed_vector
2014-03-19 wenzelm 2014-03-19 tuned -- no need for slightly obscure "local" prefix;
2014-03-19 wenzelm 2014-03-19 accomodate word as part of schematic variable name;
2014-03-19 wenzelm 2014-03-19 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
2014-03-19 wenzelm 2014-03-19 tuned proofs;
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-03-19 paulson 2014-03-19 Merge
2014-03-19 paulson 2014-03-19 New complex analysis material
2014-03-19 hoelzl 2014-03-19 NEWS
2014-03-19 hoelzl 2014-03-19 further renaming in Series
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-18 wenzelm 2014-03-18 merged;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement;
2014-03-18 wenzelm 2014-03-18 simplified (despite 70898d016538);
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 tuned proofs;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement; more antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
2014-03-18 wenzelm 2014-03-18 more antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified bootstrap process: switch to ML with context and antiquotations earlier;
2014-03-18 wenzelm 2014-03-18 more markup for improper elements;
2014-03-18 wenzelm 2014-03-18 tuned signature;
2014-03-18 wenzelm 2014-03-18 unused;
2014-03-18 wenzelm 2014-03-18 tuned signature -- rearranged modules;
2014-03-18 wenzelm 2014-03-18 tuned proofs;
2014-03-17 wenzelm 2014-03-17 back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups; discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828); more explicit shutdown;
2014-03-18 huffman 2014-03-18 remove unnecessary finiteness assumptions from lemmas about setsum
2014-03-18 huffman 2014-03-18 adapt to Isabelle/c726ecfb22b6