2012-09-15 haftmann 2012-09-15 typeclass formalising bounded subtraction
2012-09-15 haftmann 2012-09-15 dropped some unused identifiers
2012-09-15 traytel 2012-09-15 export rel_mono theorem
2012-09-14 blanchet 2012-09-14 merged two unfold steps
2012-09-14 blanchet 2012-09-14 took out one rotate_tac
2012-09-14 blanchet 2012-09-14 killed spurious rotate_tac; use auto instead of blast
2012-09-14 blanchet 2012-09-14 moved blast tactic to where it is actually needed
2012-09-14 blanchet 2012-09-14 fixed bug in "mk_map" for the "fun" case
2012-09-14 blanchet 2012-09-14 correct generalization to 3 or more mutually recursive datatypes
2012-09-14 blanchet 2012-09-14 provide more guidance, exploiting our knowledge of the goal
2012-09-14 blanchet 2012-09-14 fixed issue with bound variables in prem prems + tuning
2012-09-14 blanchet 2012-09-14 use right version of "mk_UnIN"
2012-09-14 blanchet 2012-09-14 select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14 blanchet 2012-09-14 tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14 wenzelm 2012-09-14 tuned proofs;
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 ("[]"))