2012-09-14 blanchet moved blast tactic to where it is actually needed
2012-09-14 blanchet fixed bug in "mk_map" for the "fun" case
2012-09-14 blanchet correct generalization to 3 or more mutually recursive datatypes
2012-09-14 blanchet provide more guidance, exploiting our knowledge of the goal
2012-09-14 blanchet fixed issue with bound variables in prem prems + tuning
2012-09-14 blanchet use right version of "mk_UnIN"
2012-09-14 blanchet select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14 blanchet tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14 wenzelm tuned proofs;
2012-09-14 wenzelm merged
2012-09-14 blanchet polished the induction
2012-09-14 blanchet put the flat at the right place (to avoid exceptions)
2012-09-14 blanchet fixed variable exporting problem
2012-09-14 blanchet compile
2012-09-14 blanchet added induct tactic
2012-09-14 blanchet tuning
2012-09-14 blanchet renamed "mk_UnN" to "mk_UnIN"
2012-09-14 blanchet merged two commands
2012-09-14 blanchet 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 distinguish between nested and nesting BNFs
2012-09-14 blanchet make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14 blanchet 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 no longer react on global_settings (cf. 34ac36642a31);
2012-09-14 wenzelm refined output panel: more value-oriented approach to update and caret focus;
2012-09-14 wenzelm clarified markup names;
2012-09-14 wenzelm more general Document_Model.point_range;
2012-09-14 wenzelm more static handling of rendering options;
2012-09-14 wenzelm tuned options (again);
2012-09-14 wenzelm more scalable option-group;
2012-09-14 nipkow tuned
2012-09-13 wenzelm merged
2012-09-13 wenzelm tuned proofs;
2012-09-13 hoelzl remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced
2012-09-13 wenzelm workaround for HOL-Mirabelle-ex oddities;
2012-09-13 wenzelm instructions for quick start in 20min;
2012-09-13 wenzelm more liberal init_components: base dir may get created later when resolving missing components;
2012-09-13 wenzelm more efficient painting based on cached result;
2012-09-13 wenzelm more standard init_components -- particularly important to pick up correct jdk/scala version;
2012-09-13 nipkow tuned
2012-09-12 wenzelm merged
2012-09-12 blanchet rough and ready induction
2012-09-12 blanchet nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
2012-09-12 wenzelm 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 eliminated some old material that is unused in the visible universe;
2012-09-12 blanchet tuning
2012-09-12 blanchet set up things for (co)induction sugar
2012-09-12 blanchet tuning
2012-09-12 blanchet added sumEN_tupled_balanced
2012-09-12 wenzelm load fonts into JavaFX as well;
2012-09-12 wenzelm some support for actual HTML rendering;
2012-09-12 wenzelm merged
2012-09-12 blanchet free variable name tuning
2012-09-12 blanchet reuse generated names (they look better + slightly more efficient)
2012-09-12 blanchet desambiguate grammar (e.g. for Nil's mixfix ("[]"))
2012-09-12 blanchet avoided duplicate lemma
2012-09-12 blanchet put an underscore between names, for compatibility with old package (and also because it makes sense)
2012-09-12 blanchet got rid of metis calls
2012-09-12 blanchet tuning
2012-09-12 wenzelm removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-12 wenzelm standardized ML aliases;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip