Wed, 30 Jul 2008 07:33:58 +0200 haftmann improved morphism
Wed, 30 Jul 2008 07:33:57 +0200 haftmann SML_imp, OCaml_imp
Wed, 30 Jul 2008 07:33:56 +0200 haftmann clarified
Wed, 30 Jul 2008 07:33:55 +0200 haftmann tuned
Tue, 29 Jul 2008 17:50:48 +0200 ballarin Zorn's Lemma for partial orders.
Tue, 29 Jul 2008 17:50:12 +0200 ballarin Definitions and some lemmas for reflexive orderings.
Tue, 29 Jul 2008 17:49:26 +0200 ballarin Lemmas added
Tue, 29 Jul 2008 16:19:49 +0200 ballarin New theory on divisibility.
Tue, 29 Jul 2008 16:19:19 +0200 ballarin Renamed theorems;
Tue, 29 Jul 2008 16:17:45 +0200 ballarin New theorems on summation.
Tue, 29 Jul 2008 16:17:13 +0200 ballarin Unit_inv_l, Unit_inv_r made [simp].
Tue, 29 Jul 2008 16:16:10 +0200 ballarin New theory on divisibility;
Tue, 29 Jul 2008 16:14:56 +0200 ballarin Unit_inv_l, Unit_inv_r made [simp];
Tue, 29 Jul 2008 14:20:22 +0200 haftmann Haskell now living in the RealWorld
Tue, 29 Jul 2008 14:07:23 +0200 haftmann corrected Pure dependency
Tue, 29 Jul 2008 13:16:54 +0200 nipkow added removeAll
Tue, 29 Jul 2008 08:15:44 +0200 haftmann tuned; explicit export of element accessors
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Tue, 29 Jul 2008 08:15:39 +0200 haftmann some steps towards explicit class target for canonical interpretation
Tue, 29 Jul 2008 08:15:38 +0200 haftmann declare
Mon, 28 Jul 2008 20:49:07 +0200 nipkow *** empty log message ***
Sun, 27 Jul 2008 20:08:16 +0200 urbanc simplified a proof
Sat, 26 Jul 2008 09:00:26 +0200 haftmann tuned function name
Sat, 26 Jul 2008 09:00:25 +0200 haftmann tuned bootstrap order
Fri, 25 Jul 2008 12:03:37 +0200 haftmann subclass now also works for subclasses with empty specificaton
Fri, 25 Jul 2008 12:03:36 +0200 haftmann dropped PureThy.note; added PureThy.add_thm
Fri, 25 Jul 2008 12:03:34 +0200 haftmann added class preorder
Fri, 25 Jul 2008 12:03:32 +0200 haftmann dropped locale (open)
Fri, 25 Jul 2008 12:03:31 +0200 haftmann added explicit root theory; some tuning
Fri, 25 Jul 2008 12:03:28 +0200 haftmann tuned
Fri, 25 Jul 2008 07:35:53 +0200 haftmann dropped locale (open)
Mon, 21 Jul 2008 16:30:49 +0200 haftmann (re-)added simp rules for (_ + _) div/mod _
Mon, 21 Jul 2008 15:27:23 +0200 haftmann (re-)added simp rules for (_ + _) div/mod _
Mon, 21 Jul 2008 15:26:26 +0200 haftmann added explicit purge_data
Mon, 21 Jul 2008 15:26:25 +0200 haftmann added code generation
Mon, 21 Jul 2008 15:26:24 +0200 haftmann fixed code generator setup
Mon, 21 Jul 2008 15:26:23 +0200 haftmann (adjusted)
Mon, 21 Jul 2008 13:37:14 +0200 chaieb Tuned and corrected ideal_tac for algebra.
Mon, 21 Jul 2008 13:37:10 +0200 chaieb Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
Mon, 21 Jul 2008 13:37:05 +0200 chaieb Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
Mon, 21 Jul 2008 13:36:59 +0200 chaieb Tuned and simplified proofs
Mon, 21 Jul 2008 13:36:44 +0200 chaieb Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
Mon, 21 Jul 2008 13:36:39 +0200 chaieb Relevant rules added to algebra's context
Sun, 20 Jul 2008 23:07:03 +0200 wenzelm renamed item to span, renamed contructors;
Sun, 20 Jul 2008 23:07:01 +0200 wenzelm adapted ThyEdit.span;
Sun, 20 Jul 2008 23:06:59 +0200 wenzelm maintain token range;
Sun, 20 Jul 2008 23:06:58 +0200 wenzelm tty loop: do not report status;
Sun, 20 Jul 2008 23:06:55 +0200 wenzelm added type range;
Sun, 20 Jul 2008 23:06:53 +0200 wenzelm renamed command span markup;
Sun, 20 Jul 2008 20:23:49 +0200 wenzelm SideKickParsedData: minimal content;
Sun, 20 Jul 2008 11:19:08 +0200 haftmann (adjusted)
Sun, 20 Jul 2008 11:10:04 +0200 haftmann (adjusted)
Sat, 19 Jul 2008 19:27:13 +0200 bulwahn added verification framework for the HeapMonad and quicksort as example for this framework
Sat, 19 Jul 2008 11:05:18 +0200 wenzelm build jedit plugin only if jedit is available;
Fri, 18 Jul 2008 22:03:20 +0200 wenzelm misc tuning;
Fri, 18 Jul 2008 18:25:57 +0200 haftmann more class instantiations
Fri, 18 Jul 2008 18:25:56 +0200 haftmann refined code generator setup for rational numbers; more simplification rules for rational numbers
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Fri, 18 Jul 2008 17:09:48 +0200 wenzelm fixed Scala path;
Thu, 17 Jul 2008 21:24:26 +0200 wenzelm tuned build order;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip