2011-01-15 berghofe [Sat, 15 Jan 2011 12:42:19 +0100] rev 41564
Include HOL-SPARK keywords
etc/isar-keywords.el

2011-01-15 berghofe [Sat, 15 Jan 2011 12:41:07 +0100] rev 41563
Include HOL-SPARK
Admin/update-keywords

2011-01-15 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.
src/HOL/Nominal/Nominal.thy src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/old_primrec.ML

2011-01-15 berghofe [Sat, 15 Jan 2011 12:35:29 +0100] rev 41561
Added new SPARK verification environment.
src/HOL/SPARK/Examples/Gcd/Gcd.adb src/HOL/SPARK/Examples/Gcd/Gcd.ads src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv src/HOL/SPARK/Examples/Liseq/Liseq.adb src/HOL/SPARK/Examples/Liseq/Liseq.ads src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.fdl src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.rls src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.siv src/HOL/SPARK/Examples/README src/HOL/SPARK/Examples/RIPEMD-160/F.thy src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy src/HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy src/HOL/SPARK/Examples/RIPEMD-160/Round.thy src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy src/HOL/SPARK/Examples/RIPEMD-160/rmd.adb src/HOL/SPARK/Examples/RIPEMD-160/rmd.ads src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_l.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_l.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_l.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_r.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_r.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_r.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.rls src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.siv src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_l.fdl src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_l.rls ...

2011-01-15 wenzelm [Sat, 15 Jan 2011 12:55:19 +0100] rev 41560
remove presently unused Isabelle application for official releases;
Admin/makedist

2011-01-15 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);
etc/proofgeneral-settings.el

2011-01-15 wenzelm [Sat, 15 Jan 2011 00:14:17 +0100] rev 41558
treat HOLCF as HOL library session, not as "logic";
lib/html/library_index_content.template

2011-01-15 wenzelm [Sat, 15 Jan 2011 00:06:01 +0100] rev 41557
increased startup-timeout to accommodate slow systems (especially Windows/Cygwin);
src/Tools/jEdit/plugin/Isabelle.props

2011-01-14 wenzelm [Fri, 14 Jan 2011 20:22:27 +0100] rev 41556
bundle main HOL image only, to save about 300 MB disk space;
Admin/makebin

2011-01-14 wenzelm [Fri, 14 Jan 2011 18:23:39 +0100] rev 41555
updated for release;
Admin/makebundle