isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Sat, 23 Jul 2011 16:12:12 +0200 tuned;

wenzelm [Sat, 23 Jul 2011 16:12:12 +0200] rev 43946

tuned;

Fri, 22 Jul 2011 07:33:34 +0200 merged

haftmann [Fri, 22 Jul 2011 07:33:34 +0200] rev 43945

merged

Fri, 22 Jul 2011 07:33:29 +0200 dropped errorneous hint

haftmann [Fri, 22 Jul 2011 07:33:29 +0200] rev 43944

dropped errorneous hint

Thu, 21 Jul 2011 22:47:13 +0200 moved some lemmas

haftmann [Thu, 21 Jul 2011 22:47:13 +0200] rev 43943

moved some lemmas

Thu, 21 Jul 2011 21:56:24 +0200 merged

haftmann [Thu, 21 Jul 2011 21:56:24 +0200] rev 43942

merged

Thu, 21 Jul 2011 18:40:31 +0200 ereal is a complete_linorder instance

haftmann [Thu, 21 Jul 2011 18:40:31 +0200] rev 43941

ereal is a complete_linorder instance

Wed, 20 Jul 2011 22:14:39 +0200 class complete_linorder

haftmann [Wed, 20 Jul 2011 22:14:39 +0200] rev 43940

class complete_linorder

Thu, 21 Jul 2011 21:29:10 +0200 make "concealed" lambda translation sound

blanchet [Thu, 21 Jul 2011 21:29:10 +0200] rev 43939

make "concealed" lambda translation sound

Thu, 21 Jul 2011 08:33:57 +0200 deactivating all quickcheck invocations until parallel invocation works safely

bulwahn [Thu, 21 Jul 2011 08:33:57 +0200] rev 43938

deactivating all quickcheck invocations until parallel invocation works safely

Thu, 21 Jul 2011 08:31:35 +0200 adapting two examples in Predicate_Compile_Examples

bulwahn [Thu, 21 Jul 2011 08:31:35 +0200] rev 43937

adapting two examples in Predicate_Compile_Examples

Wed, 20 Jul 2011 23:47:27 +0200 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned

blanchet [Wed, 20 Jul 2011 23:47:27 +0200] rev 43936

use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned

Wed, 20 Jul 2011 16:15:33 +0200 merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 20 Jul 2011 16:15:33 +0200] rev 43935

merge

Wed, 20 Jul 2011 16:14:49 +0200 Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 20 Jul 2011 16:14:49 +0200] rev 43934

Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal

Wed, 20 Jul 2011 15:42:23 +0200 add code generator setup and tests for ereal

hoelzl [Wed, 20 Jul 2011 15:42:23 +0200] rev 43933

add code generator setup and tests for ereal

Wed, 20 Jul 2011 15:09:53 +0200 removed debugging facilities accidentally left in the committed code

boehmes [Wed, 20 Jul 2011 15:09:53 +0200] rev 43932

removed debugging facilities accidentally left in the committed code

Wed, 20 Jul 2011 13:29:54 +0200 more precise dependencies

boehmes [Wed, 20 Jul 2011 13:29:54 +0200] rev 43931

more precise dependencies

Wed, 20 Jul 2011 13:27:01 +0200 merged

boehmes [Wed, 20 Jul 2011 13:27:01 +0200] rev 43930

merged

Wed, 20 Jul 2011 12:23:20 +0200 generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)

boehmes [Wed, 20 Jul 2011 12:23:20 +0200] rev 43929

generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)

Wed, 20 Jul 2011 09:23:12 +0200 moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)

boehmes [Wed, 20 Jul 2011 09:23:12 +0200] rev 43928

moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)

Wed, 20 Jul 2011 09:23:09 +0200 removed old (unused) SMT monomorphizer

boehmes [Wed, 20 Jul 2011 09:23:09 +0200] rev 43927

removed old (unused) SMT monomorphizer

Wed, 20 Jul 2011 13:24:49 +0200 added UNION

krauss [Wed, 20 Jul 2011 13:24:49 +0200] rev 43926

added UNION

Wed, 20 Jul 2011 10:48:00 +0200 merged

hoelzl [Wed, 20 Jul 2011 10:48:00 +0200] rev 43925

merged

Tue, 19 Jul 2011 14:38:48 +0200 rename Fin to enat

hoelzl [Tue, 19 Jul 2011 14:38:48 +0200] rev 43924

rename Fin to enat

Tue, 19 Jul 2011 14:38:29 +0200 add ereal to typeclass infinity

hoelzl [Tue, 19 Jul 2011 14:38:29 +0200] rev 43923

add ereal to typeclass infinity

Tue, 19 Jul 2011 14:37:49 +0200 add nat => enat coercion

hoelzl [Tue, 19 Jul 2011 14:37:49 +0200] rev 43922

add nat => enat coercion

Tue, 19 Jul 2011 14:37:09 +0200 Introduce infinity type class

hoelzl [Tue, 19 Jul 2011 14:37:09 +0200] rev 43921

Introduce infinity type class

Tue, 19 Jul 2011 14:36:12 +0200 Rename extreal => ereal

hoelzl [Tue, 19 Jul 2011 14:36:12 +0200] rev 43920

Rename extreal => ereal

Tue, 19 Jul 2011 14:35:44 +0200 rename Nat_Infinity (inat) to Extended_Nat (enat)

hoelzl [Tue, 19 Jul 2011 14:35:44 +0200] rev 43919

rename Nat_Infinity (inat) to Extended_Nat (enat)

Wed, 20 Jul 2011 10:11:08 +0200 HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 20 Jul 2011 10:11:08 +0200] rev 43918

HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.

Wed, 20 Jul 2011 08:46:17 +0200 build an image for HOL-IMP

kleing [Wed, 20 Jul 2011 08:46:17 +0200] rev 43917

build an image for HOL-IMP

(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle