2008-10-28 ballarin 2008-10-28 Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-28 haftmann 2008-10-28 restored incremental code generation
2008-10-28 haftmann 2008-10-28 slightly tuned
2008-10-28 haftmann 2008-10-28 assert that no class parameter is used as constructor
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-10-28 haftmann 2008-10-28 removed includes
2008-10-28 haftmann 2008-10-28 making SMLNJ happy
2008-10-28 paulson 2008-10-28 The metis method no longer fails because the theorem is too trivial
2008-10-28 ballarin 2008-10-28 Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-10-27 paulson 2008-10-27 metis proof
2008-10-27 ballarin 2008-10-27 New-style locale expressions with instantiation (new file expression.ML).
2008-10-27 ballarin 2008-10-27 Hide path in constant name (workaround).
2008-10-27 haftmann 2008-10-27 explicit history for equations; tuned
2008-10-27 haftmann 2008-10-27 slightly tuned
2008-10-27 haftmann 2008-10-27 added rudimentary code generation
2008-10-27 haftmann 2008-10-27 sup_bot and inf_top
2008-10-27 ballarin 2008-10-27 Extension of interface: declarations_of.
2008-10-24 haftmann 2008-10-24 simplified user-defined class syntax
2008-10-24 haftmann 2008-10-24 more clever module names for code generation
2008-10-24 haftmann 2008-10-24 "fun" gained a more uniform status
2008-10-24 haftmann 2008-10-24 simplified syntax for class parameters
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;