2008-10-24 haftmann 2008-10-24 tuned
2008-10-24 haftmann 2008-10-24 new classes "top" and "bot"
2008-10-24 haftmann 2008-10-24 tuned proof
2008-10-24 haftmann 2008-10-24 more clever module name aliasses for code generation
2008-10-24 haftmann 2008-10-24 "arbitrary" merely abbreviates undefined
2008-10-24 haftmann 2008-10-24 subst is a proper axiom again
2008-10-24 haftmann 2008-10-24 updated
2008-10-24 haftmann 2008-10-24 explicit namings for generated code
2008-10-23 wenzelm 2008-10-23 Thm.get_def;
2008-10-23 wenzelm 2008-10-23 Thm.def_name;
2008-10-23 wenzelm 2008-10-23 multithreading support only for polyml-5.2.1 or later;
2008-10-23 wenzelm 2008-10-23 renamed get_axiom_i to axiom, removed obsolete get_axiom; reduced pervasive names;
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-23 wenzelm 2008-10-23 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
2008-10-23 wenzelm 2008-10-23 adapted Susp.peek;
2008-10-23 wenzelm 2008-10-23 thread-safe version, with non-critical evaluation; do not re-evaluate failed result; misc tuning;
2008-10-23 wenzelm 2008-10-23 do not open Susp;
2008-10-23 wenzelm 2008-10-23 switched parallel sessions to polyml-5.2.1;
2008-10-23 wenzelm 2008-10-23 fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
2008-10-22 wenzelm 2008-10-22 updated to 5.2.1;
2008-10-22 haftmann 2008-10-22 prove_instantiation_exit combinators
2008-10-22 haftmann 2008-10-22 added meet_sort_typ
2008-10-22 haftmann 2008-10-22 tuned
2008-10-22 haftmann 2008-10-22 code identifier namings are no longer imperative
2008-10-22 haftmann 2008-10-22 tuned typedef interface
2008-10-22 haftmann 2008-10-22 slightly tuned
2008-10-22 haftmann 2008-10-22 fixed
2008-10-21 wenzelm 2008-10-21 less ambitious default for JEDIT_JAVA_OPTIONS;
2008-10-21 wenzelm 2008-10-21 JEDIT_OPTIONS: moved -settings to interface script (more robust);
2008-10-21 wenzelm 2008-10-21 make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
2008-10-21 berghofe 2008-10-21 Added nominal_inductive2.
2008-10-21 berghofe 2008-10-21 Example for using the generalized version of nominal_inductive.
2008-10-21 berghofe 2008-10-21 Added theory W.
2008-10-21 berghofe 2008-10-21 More general, still experimental version of nominal_inductive for avoiding sets of names.
2008-10-21 berghofe 2008-10-21 Added nominal_inductive2.ML
2008-10-21 wenzelm 2008-10-21 added jEdit settings;
2008-10-21 wenzelm 2008-10-21 tuned usage line;
2008-10-21 wenzelm 2008-10-21 Isabelle/jEdit interface wrapper.
2008-10-21 wenzelm 2008-10-21 join results in isolation;
2008-10-21 wenzelm 2008-10-21 join_results: allow CRITICAL join of finished futures; added singleton join_result;
2008-10-21 wenzelm 2008-10-21 Future.join_result;
2008-10-21 wenzelm 2008-10-21 added Future.enabled check;
2008-10-21 wenzelm 2008-10-21 ThyOutput: export some auxiliary operations;
2008-10-20 nipkow 2008-10-20 fixed proof
2008-10-20 nipkow 2008-10-20 added lemmas
2008-10-19 berghofe 2008-10-19 Names of variables in perm_eqs are now chosen more carefully to avoid clashes with name "pi".
2008-10-19 berghofe 2008-10-19 - removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML) - improved code unfold preprocessor: now uses one single simpset containing all unfolding rules - got rid of some legacy functions
2008-10-19 berghofe 2008-10-19 datatype_codegen now checks name of result type of constructor to avoid problems with overloaded constants such as 0.
2008-10-19 wenzelm 2008-10-19 run a program in a modified environment;
2008-10-17 wenzelm 2008-10-17 reactivated HOL-Matrix; minor cleanup;
2008-10-17 haftmann 2008-10-17 tuned
2008-10-17 haftmann 2008-10-17 filled remaining gaps
2008-10-17 haftmann 2008-10-17 added type antiquotation
2008-10-16 wenzelm 2008-10-16 tuned;
2008-10-16 wenzelm 2008-10-16 added dep for Concurrent/ROOT.ML;
2008-10-16 wenzelm 2008-10-16 tuned;
2008-10-16 wenzelm 2008-10-16 removed Locales;
2008-10-16 wenzelm 2008-10-16 goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16 wenzelm 2008-10-16 added translations for SORT_CONSTRAINT tuned;
2008-10-16 wenzelm 2008-10-16 conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;