2013-09-13 haftmann 2013-09-13 tuned proofs
2013-09-12 huffman 2013-09-12 merged
2013-09-12 huffman 2013-09-12 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-09-12 huffman 2013-09-12 generalize lemmas
2013-09-12 huffman 2013-09-12 remove unneeded assumption from prime_dvd_power lemmas; add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)
2013-09-12 huffman 2013-09-12 remove duplicate lemmas
2013-09-12 huffman 2013-09-12 new lemmas
2013-09-12 huffman 2013-09-12 prefer theorem name over 'long_thm_list(n)'
2013-09-12 huffman 2013-09-12 prefer attribute 'unfolded thm' to 'simplified'
2013-09-12 huffman 2013-09-12 removed outdated comments
2013-09-13 blanchet 2013-09-13 made non-co case more robust as well (cf. b6e2993fd0d3)
2013-09-13 blanchet 2013-09-13 don't wrongly destroy sum types in coiterators
2013-09-13 blanchet 2013-09-13 beware of multi-constructor datatypes (cf. 27c418b7b985)
2013-09-13 blanchet 2013-09-13 beware of single-constructor datatypes, with no discriminators
2013-09-12 traytel 2013-09-12 more robust tactic to cover another corner case (added as example);
2013-09-12 blanchet 2013-09-12 generalized data structure, for extension with SMT solver proofs
2013-09-12 blanchet 2013-09-12 prefixed types and some functions with "atp_" for disambiguation
2013-09-12 wenzelm 2013-09-12 merged;
2013-09-12 wenzelm 2013-09-12 absorb final CLASSPATH as well, such that tools might provide that by elementary means, without the "classpath" shell function (e.g. kodkodi/nitpick);
2013-09-12 wenzelm 2013-09-12 more CHECKLIST;
2013-09-12 wenzelm 2013-09-12 more robust System.getProperty with default;
2013-09-12 wenzelm 2013-09-12 generate distribution classpath for cold-start application wrappers;
2013-09-12 wenzelm 2013-09-12 reverse orientation of ISABELLE_CLASSPATH;
2013-09-12 wenzelm 2013-09-12 propagate ISABELLE_CLASSPATH;
2013-09-12 wenzelm 2013-09-12 tuned comments;
2013-09-12 wenzelm 2013-09-12 clarified directory structure;
2013-09-12 wenzelm 2013-09-12 maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources); ignore $ISABELLE_JAVA_EXT -- do not change java.ext.dirs;
2013-09-11 wenzelm 2013-09-11 more official initial class path according to sun.misc.Launcher;
2013-09-11 wenzelm 2013-09-11 provide main classpath again, notably for cold-start;
2013-09-11 wenzelm 2013-09-11 cold-start of main application even on Linux;
2013-09-11 wenzelm 2013-09-11 tuned proofs;
2013-09-11 wenzelm 2013-09-11 more explicit indication of 'done' as proof script element;
2013-09-12 blanchet 2013-09-12 made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"
2013-09-12 traytel 2013-09-12 conceal definitions of high-level constructors and (co)iterators
2013-09-12 traytel 2013-09-12 conceal low-level noted facts (+ FIXME to get rid of the notes altogether eventually)
2013-09-12 traytel 2013-09-12 buffer the notes even more
2013-09-12 traytel 2013-09-12 conceal internal bindings
2013-09-12 blanchet 2013-09-12 add a notice to myself in doc
2013-09-12 blanchet 2013-09-12 more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses
2013-09-12 blanchet 2013-09-12 unset some spurious executable flags
2013-09-12 traytel 2013-09-12 handle corner case in tactic
2013-09-12 traytel 2013-09-12 simplified derivation of in_rel
2013-09-12 traytel 2013-09-12 removed unused/inlinable theorems
2013-09-12 blanchet 2013-09-12 when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
2013-09-12 blanchet 2013-09-12 minor fixes
2013-09-12 blanchet 2013-09-12 commented out code parts leading to runtime errors due to missing gensim module
2013-09-12 blanchet 2013-09-12 invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
2013-09-12 blanchet 2013-09-12 new version of MaSh
2013-09-12 blanchet 2013-09-12 more (co)data docs
2013-09-12 blanchet 2013-09-12 avoid a keyword
2013-09-11 blanchet 2013-09-11 more (co)datatype docs
2013-09-11 blanchet 2013-09-11 killed dead code
2013-09-11 blanchet 2013-09-11 get rid of another complication in relevance filter
2013-09-11 blanchet 2013-09-11 tuning
2013-09-11 blanchet 2013-09-11 renamed config option
2013-09-11 haftmann 2013-09-11 more correct NEWS
2013-09-11 blanchet 2013-09-11 kick out totally hopeless facts after 5 iterations to speed things up
2013-09-11 blanchet 2013-09-11 reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
2013-09-11 blanchet 2013-09-11 more (co)data docs
2013-09-11 blanchet 2013-09-11 more (co)data docs