Sat, 05 Aug 2017 22:12:41 +0200 paulson final tidying up of lemma bounded_variation_absolutely_integrable_interval
Sat, 05 Aug 2017 18:16:35 +0200 paulson finally rid of finite_product_dependent
Sat, 05 Aug 2017 16:18:35 +0200 paulson more cleanup
Sat, 05 Aug 2017 12:18:25 +0200 paulson trying to disentangle bounded_variation_absolutely_integrable_interval
Fri, 04 Aug 2017 23:07:14 +0200 paulson merged
Fri, 04 Aug 2017 21:30:38 +0200 paulson more horrible proofs disentangled
Fri, 04 Aug 2017 08:13:00 +0200 haftmann tuned
Fri, 04 Aug 2017 08:12:58 +0200 haftmann more structural sharing between common target Generic_Target.init
Fri, 04 Aug 2017 08:12:57 +0200 haftmann exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
Fri, 04 Aug 2017 08:12:54 +0200 haftmann treat exit separate from regular local theory operations
Fri, 04 Aug 2017 08:12:37 +0200 haftmann provide explicit variant initializers for regular named target vs. almost-named target
Fri, 04 Aug 2017 08:12:37 +0200 haftmann prefer explicit datatype over implicit sum;
Fri, 04 Aug 2017 08:12:37 +0200 haftmann compactified output
Thu, 03 Aug 2017 12:50:03 +0200 haftmann lifting setup for char
Thu, 03 Aug 2017 12:50:02 +0200 haftmann one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
Thu, 03 Aug 2017 12:50:01 +0200 haftmann uniform namespace handling for both concrete and abstract types, following 32e0da92c786
Thu, 03 Aug 2017 12:50:00 +0200 haftmann clarified
Thu, 03 Aug 2017 12:49:59 +0200 haftmann corrected slip
Thu, 03 Aug 2017 12:49:58 +0200 haftmann tuned
Thu, 03 Aug 2017 12:49:57 +0200 haftmann work around weakness in export calculation when generating OCaml code
Thu, 03 Aug 2017 12:49:55 +0200 haftmann tuned
Thu, 03 Aug 2017 23:43:17 +0200 blanchet pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
Thu, 03 Aug 2017 23:43:17 +0200 blanchet updated CVC4 component to official 1.5 release
Thu, 03 Aug 2017 23:06:36 +0200 paulson merged
Thu, 03 Aug 2017 21:38:05 +0200 paulson eliminated more "guess", etc.
Thu, 03 Aug 2017 14:15:25 +0200 paulson merged
Thu, 03 Aug 2017 14:15:06 +0200 paulson more tidying
Thu, 03 Aug 2017 11:29:08 +0200 paulson more tidying up
Thu, 03 Aug 2017 10:52:13 +0200 paulson merged
Thu, 03 Aug 2017 08:09:15 +0200 paulson merged
Wed, 02 Aug 2017 23:15:15 +0200 paulson removed all "guess"
Thu, 03 Aug 2017 23:03:44 +0200 nipkow tuned
Thu, 03 Aug 2017 11:38:55 +0200 nipkow merged
Thu, 03 Aug 2017 09:30:09 +0200 nipkow added lemmas
Wed, 02 Aug 2017 20:33:39 +0200 haftmann simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
Thu, 03 Aug 2017 07:31:25 +0200 nipkow merged
Wed, 02 Aug 2017 18:22:02 +0200 nipkow generalized lemma
Tue, 01 Aug 2017 20:38:39 +0200 haftmann tuned references
Wed, 02 Aug 2017 16:31:42 +0200 paulson fixed another horrible proof
Tue, 01 Aug 2017 22:19:37 +0200 wenzelm misc tuning and modernization;
Tue, 01 Aug 2017 17:33:04 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Aug 2017 17:30:02 +0200 wenzelm misc tuning and modernization;
Tue, 01 Aug 2017 10:28:42 +0200 nipkow new lemma
Tue, 01 Aug 2017 07:26:23 +0200 boehmes more explicit Argo proof traces; more correct proof replay for term applications
Mon, 31 Jul 2017 15:38:21 +0100 paulson more cleanup of Tagged_Division
Sun, 30 Jul 2017 21:44:23 +0100 paulson partial cleanup of the horrible Tagged_Division
Fri, 28 Jul 2017 15:36:32 +0100 blanchet introduced option for nat-as-int in SMT
Thu, 27 Jul 2017 15:22:35 +0100 paulson polytopes: simplical subdivisions, etc.
Wed, 26 Jul 2017 16:07:45 +0100 paulson New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
Wed, 26 Jul 2017 13:36:36 +0100 paulson moved transitive_stepwise_le into Nat, where it belongs
Mon, 24 Jul 2017 16:50:46 +0100 paulson refactored some HORRIBLE integration proofs
Thu, 20 Jul 2017 23:59:09 +0200 Lars Hupel merged
Thu, 20 Jul 2017 17:13:17 +0200 Lars Hupel improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Thu, 20 Jul 2017 15:41:01 +0200 Lars Hupel tuned code setup
Thu, 20 Jul 2017 16:28:43 +0100 blanchet strengthened tactic
Thu, 20 Jul 2017 14:05:29 +0100 paulson Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
Wed, 19 Jul 2017 22:56:16 +0100 blanchet strengthened tactic (for 'fun' BNF)
Wed, 19 Jul 2017 16:41:26 +0100 paulson new material: Colinearity, convex sets, polytopes
Tue, 18 Jul 2017 11:35:32 +0200 eberlm poles and residues of the Gamma function
Tue, 18 Jul 2017 08:54:49 +0200 Andreas Lochbihler merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 tip