isabelle: Changelog

unused_thms no longer compares propositions, since this is no longer needed and did not work properly any longer after the addition of class constraints to propositions.

Sat, 15 Jan 2011 12:42:19 +0100 Include HOL-SPARK keywords

changeset

berghofe [Sat, 15 Jan 2011 12:42:19 +0100] rev 41564

Include HOL-SPARK keywords

Sat, 15 Jan 2011 12:41:07 +0100 Include HOL-SPARK

changeset

berghofe [Sat, 15 Jan 2011 12:41:07 +0100] rev 41563

Include HOL-SPARK

Sat, 15 Jan 2011 12:38:56 +0100 Finally removed old primrec package, since Primrec.add_primrec_global

changeset

berghofe [Sat, 15 Jan 2011 12:38:56 +0100] rev 41562

Finally removed old primrec package, since Primrec.add_primrec_global can be used instead.

Sat, 15 Jan 2011 12:35:29 +0100 Added new SPARK verification environment.

changeset

berghofe [Sat, 15 Jan 2011 12:35:29 +0100] rev 41561

Added new SPARK verification environment.

Sat, 15 Jan 2011 12:55:19 +0100 remove presently unused Isabelle application for official releases;

changeset

wenzelm [Sat, 15 Jan 2011 12:55:19 +0100] rev 41560

remove presently unused Isabelle application for official releases;

Sat, 15 Jan 2011 12:19:07 +0100 hardwired default for proof-shell-quit-timeout (PG 4.1 provides rather low value);

changeset

wenzelm [Sat, 15 Jan 2011 12:19:07 +0100] rev 41559

hardwired default for proof-shell-quit-timeout (PG 4.1 provides rather low value);

Sat, 15 Jan 2011 00:14:17 +0100 treat HOLCF as HOL library session, not as "logic";

changeset

wenzelm [Sat, 15 Jan 2011 00:14:17 +0100] rev 41558

treat HOLCF as HOL library session, not as "logic";

Sat, 15 Jan 2011 00:06:01 +0100 increased startup-timeout to accommodate slow systems (especially Windows/Cygwin);

changeset

wenzelm [Sat, 15 Jan 2011 00:06:01 +0100] rev 41557

increased startup-timeout to accommodate slow systems (especially Windows/Cygwin);

Fri, 14 Jan 2011 20:22:27 +0100 bundle main HOL image only, to save about 300 MB disk space;

changeset

wenzelm [Fri, 14 Jan 2011 20:22:27 +0100] rev 41556

bundle main HOL image only, to save about 300 MB disk space;

Fri, 14 Jan 2011 18:23:39 +0100 updated for release;

changeset

wenzelm [Fri, 14 Jan 2011 18:23:39 +0100] rev 41555

updated for release;

Fri, 14 Jan 2011 17:20:36 +0100 adjusted mira configuration

changeset

haftmann [Fri, 14 Jan 2011 17:20:36 +0100] rev 41554

adjusted mira configuration

Fri, 14 Jan 2011 16:14:51 +0100 merged

changeset

wenzelm [Fri, 14 Jan 2011 16:14:51 +0100] rev 41553

merged

Fri, 14 Jan 2011 16:01:29 +0100 global "prems" is legacy feature;

changeset

wenzelm [Fri, 14 Jan 2011 16:01:29 +0100] rev 41552

global "prems" is legacy feature;

Fri, 14 Jan 2011 16:00:11 +0100 tuned markup;

changeset

wenzelm [Fri, 14 Jan 2011 16:00:11 +0100] rev 41551

tuned markup;

Fri, 14 Jan 2011 15:44:47 +0100 eliminated global prems;

changeset

wenzelm [Fri, 14 Jan 2011 15:44:47 +0100] rev 41550

eliminated global prems; tuned proofs;

Fri, 14 Jan 2011 15:43:04 +0100 more precise import;

changeset

wenzelm [Fri, 14 Jan 2011 15:43:04 +0100] rev 41549

more precise import; eliminated global prems;

Fri, 14 Jan 2011 13:58:07 +0100 Thy_Load.begin_theory: maintain source specification of imports;

changeset

wenzelm [Fri, 14 Jan 2011 13:58:07 +0100] rev 41548

Thy_Load.begin_theory: maintain source specification of imports; Thy_Info.register_thy: reconstruct deps using original imports (important for ProofGeneral.inform_file_processed);

Fri, 14 Jan 2011 16:00:13 +0100 merged

changeset

hoelzl [Fri, 14 Jan 2011 16:00:13 +0100] rev 41547

merged

Fri, 14 Jan 2011 15:59:49 +0100 integral on lebesgue measure is extension of integral on borel measure

changeset

hoelzl [Fri, 14 Jan 2011 15:59:49 +0100] rev 41546

integral on lebesgue measure is extension of integral on borel measure

Fri, 14 Jan 2011 15:56:42 +0100 tuned formalization of subalgebra

changeset

hoelzl [Fri, 14 Jan 2011 15:56:42 +0100] rev 41545

tuned formalization of subalgebra