5 weeks ago haftmann 2020-05-24 better closeup and more consistent terminology
5 weeks ago wenzelm 2020-05-24 merged
5 weeks ago wenzelm 2020-05-24 proper stack_limit;
5 weeks ago wenzelm 2020-05-24 clarified signature;
5 weeks ago wenzelm 2020-05-24 more accurate classpath for "isabelle scala";
5 weeks ago wenzelm 2020-05-24 proper check of registered Scala functions;
5 weeks ago wenzelm 2020-05-24 asynchronous build_session: notably for Scala.fulfill protocol commands during run;
5 weeks ago wenzelm 2020-05-24 clarified build_session protocol;
5 weeks ago wenzelm 2020-05-24 clarified signature;
5 weeks ago wenzelm 2020-05-24 clarified name;
5 weeks ago wenzelm 2020-05-24 more robust: explicit check for PIDE session;
5 weeks ago wenzelm 2020-05-24 tuned signature;
5 weeks ago wenzelm 2020-05-24 unused;
5 weeks ago wenzelm 2020-05-23 tuned signature;
5 weeks ago wenzelm 2020-05-23 check Scala source snippets from ML;
5 weeks ago wenzelm 2020-05-23 more robust isabelle.Functions --- avoid Java reflection with unclear class/object treatment;
5 weeks ago wenzelm 2020-05-23 init default context;
5 weeks ago wenzelm 2020-05-23 tuned message;
5 weeks ago wenzelm 2020-05-23 clarified signature;
5 weeks ago wenzelm 2020-05-23 tuned;
5 weeks ago wenzelm 2020-05-23 more brackets (see 2e8af171887f);
5 weeks ago wenzelm 2020-05-23 tuned message;
6 weeks ago wenzelm 2020-05-22 clarified signature; more operations;
6 weeks ago wenzelm 2020-05-22 unused;
6 weeks ago wenzelm 2020-05-22 more robust, notably for "isabelle scala";
6 weeks ago wenzelm 2020-05-22 clarified signature;
5 weeks ago nipkow 2020-05-24 reorganised sorted_set_of_list
5 weeks ago nipkow 2020-05-24 merged
5 weeks ago nipkow 2020-05-24 simpler inductions
5 weeks ago paulson 2020-05-23 a few new lemmas about functions
5 weeks ago nipkow 2020-05-22 comment makes no sense
6 weeks ago nipkow 2020-05-22 added simp lemma
6 weeks ago haftmann 2020-05-21 slightly more specific implementations
6 weeks ago haftmann 2020-05-21 tuned module name space for generated code
6 weeks ago nipkow 2020-05-21 unused alias
6 weeks ago haftmann 2020-05-20 generalized and augmented
6 weeks ago wenzelm 2020-05-20 clarified signature;
6 weeks ago wenzelm 2020-05-20 clarified modules;
6 weeks ago paulson 2020-05-20 A few new theorems, plus some tidying up
6 weeks ago haftmann 2020-05-20 corrected spelling and tuned whitespace
6 weeks ago nipkow 2020-05-19 tuned
6 weeks ago wenzelm 2020-05-18 follow Phabricator update 2020 Week 19;
6 weeks ago nipkow 2020-05-17 another AVL tree version
7 weeks ago Manuel Eberl 2020-05-15 added missing preprocessing step for extraction (due to Stefan Berghofer)
7 weeks ago Manuel Eberl 2020-05-13 new HOL simproc: eliminate_false_implies
7 weeks ago nipkow 2020-05-14 added lemma
7 weeks ago Manuel Eberl 2020-05-14 Tuned some proofs in HOL-Analysis
7 weeks ago paulson 2020-05-14 The Uniq quantifier for FOL too
7 weeks ago Manuel Eberl 2020-05-13 generalised pigeonhole principle in HOL-Library.FuncSet
7 weeks ago Manuel Eberl 2020-05-13 new constant power_int in HOL
8 weeks ago Manuel Eberl 2020-05-04 New HOL simproc 'datatype_no_proper_subterm'
7 weeks ago paulson 2020-05-12 merged
7 weeks ago paulson 2020-05-12 Fixes for Sup{} = (0::nat)
7 weeks ago paulson 2020-05-12 abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
7 weeks ago wenzelm 2020-05-12 clarified session imports: avoid bulky HOL-Library image;
7 weeks ago wenzelm 2020-05-12 tuned -- avoid warning;
7 weeks ago nipkow 2020-05-12 "app" -> "join" for RBTs
7 weeks ago nipkow 2020-05-12 "app" -> "join" for uniformity with Join theory; tuned defs
7 weeks ago nipkow 2020-05-11 added top-level functions and tuned
7 weeks ago paulson 2020-05-11 the Uniq quantifier