2015-03-16 traytel 2015-03-16 BNF relators preserve reflexivity
2015-03-16 blanchet 2015-03-16 export more ML functions
2015-03-16 wenzelm 2015-03-16 merged
2015-03-16 wenzelm 2015-03-16 suppress semantic completion in errors of batch build -- avoid junk in log files;
2015-03-16 blanchet 2015-03-16 updated docs
2015-03-16 blanchet 2015-03-16 clarified documentation
2015-03-16 wenzelm 2015-03-16 proper headers;
2015-03-16 wenzelm 2015-03-16 merged
2015-03-16 wenzelm 2015-03-16 tuned message -- include completion;
2015-03-16 wenzelm 2015-03-16 support for completion reports produced in Scala (inlined into messages);
2015-03-16 wenzelm 2015-03-16 more precises positions; more permissive imports;
2015-03-16 wenzelm 2015-03-16 avoid duplicate header errors, more precise positions; tuned signature;
2015-03-16 wenzelm 2015-03-16 tuned protocol -- resolve command positions in ML;
2015-03-16 wenzelm 2015-03-16 clarified modules;
2015-03-16 hoelzl 2015-03-16 add inequalities (move from AFP/Amortized_Complexity)
2015-03-15 blanchet 2015-03-15 merge
2015-03-15 blanchet 2015-03-15 inlining threshold
2015-03-15 blanchet 2015-03-15 avoid controversial Pirate syntax
2015-03-15 wenzelm 2015-03-15 more markup, which helps to create missing imports;
2015-03-15 wenzelm 2015-03-15 tuned signature;
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