Fri, 31 Oct 2008 10:39:04 +0100 berghofe Theorem "_" is now stored with open derivation.
Fri, 31 Oct 2008 10:37:34 +0100 berghofe Removed argument prf2 in rewrite rules for equal_elim to make them applicable
Fri, 31 Oct 2008 10:35:30 +0100 berghofe Replaced arbitrary by undefined.
Thu, 30 Oct 2008 10:57:45 +0100 ballarin Dropped context element 'includes'.
Wed, 29 Oct 2008 15:32:58 +0100 haftmann adapted to strict pattern discipline
Wed, 29 Oct 2008 11:33:40 +0100 haftmann explicit check for pattern discipline before code translation
Tue, 28 Oct 2008 17:53:46 +0100 ballarin Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
Tue, 28 Oct 2008 16:59:02 +0100 haftmann restored incremental code generation
Tue, 28 Oct 2008 16:59:01 +0100 haftmann slightly tuned
Tue, 28 Oct 2008 16:59:00 +0100 haftmann assert that no class parameter is used as constructor
Tue, 28 Oct 2008 16:58:59 +0100 haftmann cleanup code default attribute
Tue, 28 Oct 2008 12:29:57 +0100 haftmann removed includes
Tue, 28 Oct 2008 12:28:14 +0100 haftmann making SMLNJ happy
Tue, 28 Oct 2008 11:05:44 +0100 paulson The metis method no longer fails because the theorem is too trivial
Tue, 28 Oct 2008 11:03:07 +0100 ballarin Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
Mon, 27 Oct 2008 18:14:34 +0100 paulson metis proof
Mon, 27 Oct 2008 16:23:54 +0100 ballarin New-style locale expressions with instantiation (new file expression.ML).
Mon, 27 Oct 2008 16:20:52 +0100 ballarin Hide path in constant name (workaround).
Mon, 27 Oct 2008 16:15:50 +0100 haftmann explicit history for equations; tuned
Mon, 27 Oct 2008 16:15:49 +0100 haftmann slightly tuned
Mon, 27 Oct 2008 16:15:48 +0100 haftmann added rudimentary code generation
Mon, 27 Oct 2008 16:15:47 +0100 haftmann sup_bot and inf_top
Mon, 27 Oct 2008 16:14:51 +0100 ballarin Extension of interface: declarations_of.
Fri, 24 Oct 2008 17:51:36 +0200 haftmann simplified user-defined class syntax
Fri, 24 Oct 2008 17:51:35 +0200 haftmann more clever module names for code generation
Fri, 24 Oct 2008 17:48:42 +0200 haftmann "fun" gained a more uniform status
Fri, 24 Oct 2008 17:48:40 +0200 haftmann simplified syntax for class parameters
Fri, 24 Oct 2008 17:48:39 +0200 haftmann tuned
Fri, 24 Oct 2008 17:48:37 +0200 haftmann new classes "top" and "bot"
Fri, 24 Oct 2008 17:48:36 +0200 haftmann tuned proof
Fri, 24 Oct 2008 17:48:35 +0200 haftmann more clever module name aliasses for code generation
Fri, 24 Oct 2008 17:48:34 +0200 haftmann "arbitrary" merely abbreviates undefined
Fri, 24 Oct 2008 17:48:33 +0200 haftmann subst is a proper axiom again
Fri, 24 Oct 2008 10:41:15 +0200 haftmann updated
Fri, 24 Oct 2008 10:41:13 +0200 haftmann explicit namings for generated code
Thu, 23 Oct 2008 16:07:03 +0200 wenzelm Thm.get_def;
Thu, 23 Oct 2008 15:28:39 +0200 wenzelm Thm.def_name;
Thu, 23 Oct 2008 15:28:08 +0200 wenzelm multithreading support only for polyml-5.2.1 or later;
Thu, 23 Oct 2008 15:28:05 +0200 wenzelm renamed get_axiom_i to axiom, removed obsolete get_axiom;
Thu, 23 Oct 2008 15:28:01 +0200 wenzelm renamed Thm.get_axiom_i to Thm.axiom;
Thu, 23 Oct 2008 14:22:16 +0200 wenzelm renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
Thu, 23 Oct 2008 13:52:28 +0200 wenzelm adapted Susp.peek;
Thu, 23 Oct 2008 13:52:27 +0200 wenzelm thread-safe version, with non-critical evaluation;
Thu, 23 Oct 2008 13:52:26 +0200 wenzelm do not open Susp;
Thu, 23 Oct 2008 13:51:54 +0200 wenzelm switched parallel sessions to polyml-5.2.1;
Thu, 23 Oct 2008 00:24:31 +0200 wenzelm fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
Wed, 22 Oct 2008 21:25:00 +0200 wenzelm updated to 5.2.1;
Wed, 22 Oct 2008 14:15:48 +0200 haftmann prove_instantiation_exit combinators
Wed, 22 Oct 2008 14:15:47 +0200 haftmann added meet_sort_typ
Wed, 22 Oct 2008 14:15:46 +0200 haftmann tuned
Wed, 22 Oct 2008 14:15:45 +0200 haftmann code identifier namings are no longer imperative
Wed, 22 Oct 2008 14:15:44 +0200 haftmann tuned typedef interface
Wed, 22 Oct 2008 14:15:43 +0200 haftmann slightly tuned
Wed, 22 Oct 2008 14:15:42 +0200 haftmann fixed
Tue, 21 Oct 2008 23:54:42 +0200 wenzelm less ambitious default for JEDIT_JAVA_OPTIONS;
Tue, 21 Oct 2008 22:21:28 +0200 wenzelm JEDIT_OPTIONS: moved -settings to interface script (more robust);
Tue, 21 Oct 2008 21:59:22 +0200 wenzelm make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
Tue, 21 Oct 2008 21:22:31 +0200 berghofe Added nominal_inductive2.
Tue, 21 Oct 2008 21:22:02 +0200 berghofe Example for using the generalized version of nominal_inductive.
Tue, 21 Oct 2008 21:20:46 +0200 berghofe Added theory W.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip