2012-09-14 wenzelm 2012-09-14 merged
2012-09-14 blanchet 2012-09-14 polished the induction
2012-09-14 blanchet 2012-09-14 put the flat at the right place (to avoid exceptions)
2012-09-14 blanchet 2012-09-14 fixed variable exporting problem
2012-09-14 blanchet 2012-09-14 compile
2012-09-14 blanchet 2012-09-14 added induct tactic
2012-09-14 blanchet 2012-09-14 tuning
2012-09-14 blanchet 2012-09-14 renamed "mk_UnN" to "mk_UnIN"
2012-09-14 blanchet 2012-09-14 merged two commands
2012-09-14 blanchet 2012-09-14 allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
2012-09-14 blanchet 2012-09-14 distinguish between nested and nesting BNFs
2012-09-14 blanchet 2012-09-14 make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14 blanchet 2012-09-14 derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
2012-09-14 wenzelm 2012-09-14 no longer react on global_settings (cf. 34ac36642a31);
2012-09-14 wenzelm 2012-09-14 refined output panel: more value-oriented approach to update and caret focus;
2012-09-14 wenzelm 2012-09-14 clarified markup names;
2012-09-14 wenzelm 2012-09-14 more general Document_Model.point_range; more general Document_View.Active_Area; eliminated dead popup material;
2012-09-14 wenzelm 2012-09-14 more static handling of rendering options;
2012-09-14 wenzelm 2012-09-14 tuned options (again);
2012-09-14 wenzelm 2012-09-14 more scalable option-group;
2012-09-14 nipkow 2012-09-14 tuned
2012-09-13 wenzelm 2012-09-13 merged
2012-09-13 wenzelm 2012-09-13 tuned proofs;
2012-09-13 hoelzl 2012-09-13 remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced
2012-09-13 wenzelm 2012-09-13 workaround for HOL-Mirabelle-ex oddities;
2012-09-13 wenzelm 2012-09-13 instructions for quick start in 20min;
2012-09-13 wenzelm 2012-09-13 more liberal init_components: base dir may get created later when resolving missing components;
2012-09-13 wenzelm 2012-09-13 more efficient painting based on cached result;
2012-09-13 wenzelm 2012-09-13 more standard init_components -- particularly important to pick up correct jdk/scala version;
2012-09-13 nipkow 2012-09-13 tuned
2012-09-12 wenzelm 2012-09-12 merged
2012-09-12 blanchet 2012-09-12 rough and ready induction
2012-09-12 blanchet 2012-09-12 nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
2012-09-12 wenzelm 2012-09-12 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-09-12 wenzelm 2012-09-12 eliminated some old material that is unused in the visible universe;
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 set up things for (co)induction sugar
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 added sumEN_tupled_balanced
2012-09-12 wenzelm 2012-09-12 load fonts into JavaFX as well;
2012-09-12 wenzelm 2012-09-12 some support for actual HTML rendering;
2012-09-12 wenzelm 2012-09-12 merged
2012-09-12 blanchet 2012-09-12 free variable name tuning
2012-09-12 blanchet 2012-09-12 reuse generated names (they look better + slightly more efficient)
2012-09-12 blanchet 2012-09-12 desambiguate grammar (e.g. for Nil's mixfix ("[]"))
2012-09-12 blanchet 2012-09-12 avoided duplicate lemma
2012-09-12 blanchet 2012-09-12 put an underscore between names, for compatibility with old package (and also because it makes sense)
2012-09-12 blanchet 2012-09-12 got rid of metis calls
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 wenzelm 2012-09-12 removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-12 wenzelm 2012-09-12 standardized ML aliases;
2012-09-12 wenzelm 2012-09-12 tuned headers;
2012-09-12 wenzelm 2012-09-12 avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
2012-09-12 wenzelm 2012-09-12 discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
2012-09-12 wenzelm 2012-09-12 more robust interrupt handling;
2012-09-12 wenzelm 2012-09-12 some attempts to synchronize ROOT/files and document/build;
2012-09-12 wenzelm 2012-09-12 tuned error;
2012-09-12 traytel 2012-09-12 option_pred characterization
2012-09-12 traytel 2012-09-12 true vs. True in pattern matching
2012-09-12 blanchet 2012-09-12 reduced theory dependencies