Mon, 04 Aug 2008 18:57:35 +0200 berghofe Quoted terms in consts_code declarations are now preprocessed as well.
Mon, 04 Aug 2008 18:56:55 +0200 berghofe Exported eval_wrapper.
Mon, 04 Aug 2008 18:56:22 +0200 berghofe - corrected bogus comment for function inst_conj_all
Mon, 04 Aug 2008 18:24:27 +0200 krauss removed dead code
Mon, 04 Aug 2008 17:13:34 +0200 wenzelm simplified prepare_command;
Mon, 04 Aug 2008 17:13:33 +0200 wenzelm Isar.command: explicitly set transaction position, as required for prepare_command errors;
Mon, 04 Aug 2008 10:37:33 +0200 ballarin Updated locale tests.
Fri, 01 Aug 2008 18:10:52 +0200 ballarin Generalised polynomial lemmas from cring to ring.
Fri, 01 Aug 2008 17:41:37 +0200 ballarin Removed import and lparams from locale record.
Fri, 01 Aug 2008 12:57:50 +0200 nipkow made setsum executable on int.
Thu, 31 Jul 2008 09:49:21 +0200 ballarin Tuned (for the sake of a meaningless log entry).
Wed, 30 Jul 2008 19:03:33 +0200 ballarin New locales for orders and lattices where the equivalence relation is not restricted to equality.
Wed, 30 Jul 2008 16:07:00 +0200 nipkow added hint about writing "x : set xs".
Wed, 30 Jul 2008 07:34:01 +0200 haftmann simple lifters
Wed, 30 Jul 2008 07:34:00 +0200 haftmann dropped imperative monad bind
Wed, 30 Jul 2008 07:33:59 +0200 haftmann facts_of
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip