Tue, 15 Jan 2008 02:38:13 +0100 huffman add instance for class bifinite
Tue, 15 Jan 2008 02:20:47 +0100 huffman clean up some proofs;
Tue, 15 Jan 2008 02:18:01 +0100 huffman declare cpair_strict [simp]
Mon, 14 Jan 2008 23:19:28 +0100 isatest make at-sml-dev experimental
Mon, 14 Jan 2008 21:42:58 +0100 huffman added bifinite class instance
Mon, 14 Jan 2008 21:16:06 +0100 huffman add bifinite instances
Mon, 14 Jan 2008 21:15:20 +0100 huffman add class bifinite_cpo for possibly-unpointed bifinite domains
Mon, 14 Jan 2008 20:45:10 +0100 huffman cleaned up instance proofs
Mon, 14 Jan 2008 20:35:52 +0100 huffman new-style instantiation proof for unit :: po
Mon, 14 Jan 2008 20:28:59 +0100 huffman class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
Mon, 14 Jan 2008 20:04:40 +0100 huffman simplified chfin instance proof
Mon, 14 Jan 2008 19:26:41 +0100 huffman new theory of powerdomains
Mon, 14 Jan 2008 19:26:01 +0100 huffman new theory of bifinite domains
Mon, 14 Jan 2008 19:25:21 +0100 huffman new-style class instantiation
Mon, 14 Jan 2008 18:25:20 +0100 huffman added lemmas lub_distribs
Mon, 14 Jan 2008 16:15:55 +0100 nipkow *** empty log message ***
Mon, 14 Jan 2008 11:45:57 +0100 nipkow *** empty log message ***
Mon, 14 Jan 2008 03:58:30 +0100 huffman compact_chfin is now declared simp
Mon, 14 Jan 2008 03:56:31 +0100 huffman use new-style class for po
Mon, 14 Jan 2008 03:54:31 +0100 huffman add lemma contI2
Mon, 14 Jan 2008 03:49:53 +0100 huffman converted adm_all and adm_ball to rule_format; cleaned up
Sun, 13 Jan 2008 11:54:36 +0100 berghofe Equations for constants without arguments are now declared using
Thu, 10 Jan 2008 20:53:06 +0100 huffman new theory defining set as a pcpo
Thu, 10 Jan 2008 19:28:02 +0100 berghofe Test data generation and conversion to terms are now more closely
Thu, 10 Jan 2008 19:25:08 +0100 berghofe New example involving functions.
Thu, 10 Jan 2008 19:24:23 +0100 berghofe Now uses more carefully designed simpsets to prevent proofs from
Thu, 10 Jan 2008 19:21:56 +0100 berghofe Test data generation and conversion to terms is now more closely
Thu, 10 Jan 2008 19:18:14 +0100 berghofe Eliminated DatatypeAux.dest_TFree to avoid clashes
Thu, 10 Jan 2008 19:10:37 +0100 berghofe Added nil_const and cons_const.
Thu, 10 Jan 2008 19:10:08 +0100 berghofe Added test data generator for function type (from Pure/codegen.ML).
Thu, 10 Jan 2008 19:09:21 +0100 berghofe New interface for test data generators.
Thu, 10 Jan 2008 17:06:41 +0100 huffman declare ch2ch_LAM [simp]
Thu, 10 Jan 2008 08:21:03 +0100 haftmann added overloading target
Thu, 10 Jan 2008 05:43:20 +0100 huffman new compactness lemmas; removed duplicated flat_less_iff
Thu, 10 Jan 2008 05:37:18 +0100 huffman Compactness subsection with new lemmas
Thu, 10 Jan 2008 05:36:03 +0100 huffman Compactness subsection with some new lemmas
Thu, 10 Jan 2008 05:15:43 +0100 huffman new compactness lemmas
Thu, 10 Jan 2008 05:11:09 +0100 huffman new lemmas max_in_chainI, max_in_chainD
Wed, 09 Jan 2008 20:25:18 +0100 haftmann overloading target
Wed, 09 Jan 2008 19:24:15 +0100 nipkow tuned
Wed, 09 Jan 2008 19:23:50 +0100 nipkow added simp attributes/ proofs fixed
Wed, 09 Jan 2008 19:23:36 +0100 nipkow added simp attributes
Wed, 09 Jan 2008 10:56:35 +0100 nipkow Finally: no more unproven.
Wed, 09 Jan 2008 08:57:12 +0100 haftmann tuned
Wed, 09 Jan 2008 08:33:01 +0100 haftmann some more primrec
Wed, 09 Jan 2008 08:32:09 +0100 haftmann tuned
Wed, 09 Jan 2008 08:04:40 +0100 haftmann a note on syntax in class context
Wed, 09 Jan 2008 08:04:03 +0100 haftmann a note on syntax
Tue, 08 Jan 2008 23:11:08 +0100 urbanc tuned proofs
Tue, 08 Jan 2008 11:37:37 +0100 haftmann normalization conversion
Tue, 08 Jan 2008 11:37:32 +0100 haftmann tuned comment
Tue, 08 Jan 2008 11:37:30 +0100 haftmann explicit type variables for instantiation
Tue, 08 Jan 2008 11:37:29 +0100 haftmann better error reporting
Tue, 08 Jan 2008 11:37:28 +0100 haftmann tuned
Tue, 08 Jan 2008 11:37:27 +0100 haftmann refined overloading target
Tue, 08 Jan 2008 10:24:34 +0100 berghofe imp_conv_disj is now declared as a "code unfold" lemma to avoid that
Mon, 07 Jan 2008 11:40:20 +0100 wenzelm isabelle.jars: temporarily disabled, until isatest gets up-to-date java;
Mon, 07 Jan 2008 02:24:24 +0100 urbanc some pre-release tunings
Sun, 06 Jan 2008 19:18:01 +0100 wenzelm more robust console thread (cf. jedit plugin version);
Sun, 06 Jan 2008 18:09:34 +0100 wenzelm build Isabelle process wrapper;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip