2017-01-25 nipkow 2017-01-25 tuned
2017-01-24 haftmann 2017-01-24 dropped dead code
2017-01-24 haftmann 2017-01-24 ensure no duplicates after preprocessing
2017-01-24 haftmann 2017-01-24 reject polymorphic result types; formally generalized to multiple result types
2017-01-24 haftmann 2017-01-24 explicit a-priori detection of unsuitable terms for computations
2017-01-24 wenzelm 2017-01-24 more options;
2017-01-23 wenzelm 2017-01-23 tuned;
2017-01-22 haftmann 2017-01-22 experimental computations: use arbitrary generated code for RHSs, not just constants
2017-01-23 traytel 2017-01-23 tuned documentation
2017-01-22 wenzelm 2017-01-22 merged
2017-01-22 wenzelm 2017-01-22 updated to jdk-8u121;
2017-01-22 wenzelm 2017-01-22 clarified owner;
2017-01-22 wenzelm 2017-01-22 insist in proper GNU tar, to avoid subtle semantic differences;
2017-01-22 wenzelm 2017-01-22 hardlink within JVM; clarified file attributes;
2017-01-22 wenzelm 2017-01-22 tuned;
2017-01-22 wenzelm 2017-01-22 clarified operation: include dirs as well;
2017-01-22 wenzelm 2017-01-22 tuned;
2017-01-22 wenzelm 2017-01-22 tuned;
2017-01-22 wenzelm 2017-01-22 build_jdk in Scala;
2017-01-21 haftmann 2017-01-21 corrected static scope: multi-argument composition does not apply partially
2017-01-20 boehmes 2017-01-20 less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
2017-01-20 wenzelm 2017-01-20 tuned;
2017-01-20 nipkow 2017-01-20 added postorder
2017-01-20 nipkow 2017-01-20 tuned
2017-01-19 nipkow 2017-01-19 int version slicker
2017-01-19 nipkow 2017-01-19 tuned
2017-01-18 nipkow 2017-01-18 tuned
2017-01-18 wenzelm 2017-01-18 clarified theory name; tuned;
2017-01-18 paulson 2017-01-18 New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
2017-01-17 nipkow 2017-01-17 tuned
2017-01-17 wenzelm 2017-01-17 removed some old ASCII syntax;
2017-01-17 wenzelm 2017-01-17 prefer context groups;
2017-01-17 wenzelm 2017-01-17 misc tuning and modernization;
2017-01-17 wenzelm 2017-01-17 prefer context groups;
2017-01-17 wenzelm 2017-01-17 more symbols;
2017-01-17 wenzelm 2017-01-17 misc tuning and modernization;
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2017-01-17 wenzelm 2017-01-17 more symbols via abbrevs;
2017-01-16 wenzelm 2017-01-16 tuned signature;
2017-01-16 wenzelm 2017-01-16 clarified classical rules;
2017-01-16 wenzelm 2017-01-16 misc tuning and updates according to Curry-Club Dec-2016;
2017-01-16 wenzelm 2017-01-16 added option -n, e.g. useful to generate Dockerfile only;
2017-01-16 wenzelm 2017-01-16 support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
2017-01-16 wenzelm 2017-01-16 tuned -- nicer generated bash source;
2017-01-15 wenzelm 2017-01-15 afford approx. 10MB for curl, e.g. required for "isabelle components";
2017-01-15 wenzelm 2017-01-15 updated to jvm-1.8;
2017-01-15 wenzelm 2017-01-15 uniform use of ISABELLE_SCALAC_OPTIONS for scalac, notably for -Xmax-classfile-name on encrypted or docker file-systems;
2017-01-15 wenzelm 2017-01-15 clarified settings;
2017-01-15 wenzelm 2017-01-15 clarified signature: packages may be accessed in Isabelle/Scala;
2017-01-15 wenzelm 2017-01-15 tuned whitespace;
2017-01-15 wenzelm 2017-01-15 clarified packages (for z3);
2017-01-15 wenzelm 2017-01-15 proper tag syntax;
2017-01-15 wenzelm 2017-01-15 clarified packages; tuned message;
2017-01-14 wenzelm 2017-01-14 clarified packages;
2017-01-14 wenzelm 2017-01-14 more options;
2017-01-14 wenzelm 2017-01-14 do avoid suspicious Unicode;
2017-01-14 wenzelm 2017-01-14 more standard header; avoid suspicious Unicode;
2017-01-14 wenzelm 2017-01-14 build docker image from Isabelle application bundle for Linux;
2017-01-14 wenzelm 2017-01-14 tuned message;
2017-01-13 eberlm 2017-01-13 Added Circle_Area to HOL-Analysis examples