2015-03-15 wenzelm 2015-03-15 proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-15 wenzelm 2015-03-15 clarified span position;
2015-03-15 wenzelm 2015-03-15 tuned;
2015-03-15 wenzelm 2015-03-15 tuned;
2015-03-15 wenzelm 2015-03-15 hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML; tuned;
2015-03-15 wenzelm 2015-03-15 more command categories, as in ML;
2015-03-15 wenzelm 2015-03-15 tuned;
2015-03-14 wenzelm 2015-03-14 value-oriented user error, for well-defined Thy_Syntax.chop_common;
2015-03-14 wenzelm 2015-03-14 more explicit exception User_Error, with value-oriented equality;
2015-03-14 wenzelm 2015-03-14 tuned signature;
2015-03-14 wenzelm 2015-03-14 clarified positions of theory imports;
2015-03-14 wenzelm 2015-03-14 misc tuning -- more uniform ML vs. Scala;
2015-03-14 wenzelm 2015-03-14 tunes signature -- more uniform ML vs. Scala;
2015-03-14 wenzelm 2015-03-14 position parser as in ML;
2015-03-13 wenzelm 2015-03-13 tuned signature; minimal I/O on GUI thread should be OK;
2015-03-13 nipkow 2015-03-13 rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
2015-03-13 wenzelm 2015-03-13 simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;
2015-03-13 wenzelm 2015-03-13 removed junk;
2015-03-13 wenzelm 2015-03-13 tuned;
2015-03-12 wenzelm 2015-03-12 merged
2015-03-12 wenzelm 2015-03-12 clarified markup for embedded files, early before execution;
2015-03-12 wenzelm 2015-03-12 clarified command content;
2015-03-12 wenzelm 2015-03-12 tuned -- more uniform ML vs. Scala;
2015-03-12 wenzelm 2015-03-12 quote "method" to allow Eisbach using this keyword;
2015-03-12 hoelzl 2015-03-12 rel_pmf on equivalence relation
2015-03-12 Andreas Lochbihler 2015-03-12 make proofs work with 4762c690a75c
2015-03-11 hoelzl 2015-03-11 add subadditivity for Liminf on ereal
2015-03-11 Andreas Lochbihler 2015-03-11 merged
2015-03-10 Andreas Lochbihler 2015-03-10 merged
2015-03-10 Andreas Lochbihler 2015-03-10 more type class instances
2015-03-10 blanchet 2015-03-10 documented renamed theories
2015-03-10 blanchet 2015-03-10 export more functions (for future 'corec')
2015-03-10 blanchet 2015-03-10 tuning
2015-03-10 wenzelm 2015-03-10 merged
2015-03-10 wenzelm 2015-03-10 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-03-10 hoelzl 2015-03-10 generalized bind_cond_pmf_cancel
2015-03-10 paulson 2015-03-10 renaming HOL/Fact.thy -> Binomial.thy
2015-03-10 paulson 2015-03-10 Merge
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-03-10 wenzelm 2015-03-10 clarified Token.check_src: intern at most once; Method.parse_internal for Eisbach: intern method names;
2015-03-10 hoelzl 2015-03-10 add set_pmf lemmas to simpset
2015-03-10 hoelzl 2015-03-10 build pmf's on bind
2015-03-10 blanchet 2015-03-10 split into subgoals
2015-03-10 blanchet 2015-03-10 tuning
2015-03-09 wenzelm 2015-03-09 merged
2015-03-09 wenzelm 2015-03-09 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;
2015-03-09 paulson 2015-03-09 Removed the infix operator "choose" to allow HOLCF to build
2015-03-09 paulson 2015-03-09 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2015-03-09 wenzelm 2015-03-09 eliminated unused arith "verbose" flag -- tools that need options can use the context;
2015-03-09 wenzelm 2015-03-09 eliminated dead code (cf. 5e5c36b051af);
2015-03-09 wenzelm 2015-03-09 tuned;
2015-03-08 wenzelm 2015-03-08 clarified aliases;
2015-03-08 wenzelm 2015-03-08 misc tuning and simplification;
2015-03-08 wenzelm 2015-03-08 tuned;
2015-03-08 wenzelm 2015-03-08 misc tuning and simplification;
2015-03-08 wenzelm 2015-03-08 tuned;
2015-03-08 wenzelm 2015-03-08 cartouche_declaration for Eisbach;
2015-03-07 wenzelm 2015-03-07 NEWS;
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;