Thu, 27 Jan 2011 17:37:42 +0100 Added tag isa2011-test3 for changeset 55a45051b220
wenzelm [Thu, 27 Jan 2011 17:37:42 +0100] rev 41638
Added tag isa2011-test3 for changeset 55a45051b220
Thu, 27 Jan 2011 16:31:03 +0100 Tuned definition of sdiv.
berghofe [Thu, 27 Jan 2011 16:31:03 +0100] rev 41637
Tuned definition of sdiv.
Thu, 27 Jan 2011 16:24:29 +0100 CRITICAL markup for critical poking with unsynchronized references;
wenzelm [Thu, 27 Jan 2011 16:24:29 +0100] rev 41636
CRITICAL markup for critical poking with unsynchronized references;
Wed, 26 Jan 2011 20:51:09 +0100 Replaced smod by standard mod operator to reflect actual behaviour
berghofe [Wed, 26 Jan 2011 20:51:09 +0100] rev 41635
Replaced smod by standard mod operator to reflect actual behaviour of the SPARK tools.
Thu, 27 Jan 2011 12:24:00 +0100 cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm [Thu, 27 Jan 2011 12:24:00 +0100] rev 41634
cancel document execution before editing, to improve reactivity on systems with few cores;
Tue, 25 Jan 2011 22:59:03 +0100 tuned isatest settings (for Poly/ML SVN 1278);
wenzelm [Tue, 25 Jan 2011 22:59:03 +0100] rev 41633
tuned isatest settings (for Poly/ML SVN 1278);
Tue, 25 Jan 2011 22:15:03 +0100 merged
wenzelm [Tue, 25 Jan 2011 22:15:03 +0100] rev 41632
merged
Tue, 25 Jan 2011 14:06:43 +0100 do not restore old files on startup, which is potentially slow due to automatic rechecking;
wenzelm [Tue, 25 Jan 2011 14:06:43 +0100] rev 41631
do not restore old files on startup, which is potentially slow due to automatic rechecking; attempt to enable thick caret for improved visibility;
Tue, 25 Jan 2011 21:26:25 +0100 singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
wenzelm [Tue, 25 Jan 2011 21:26:25 +0100] rev 41630
singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
Tue, 25 Jan 2011 20:06:32 +0100 workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
wenzelm [Tue, 25 Jan 2011 20:06:32 +0100] rev 41629
workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
Mon, 24 Jan 2011 21:30:33 +0100 improved README -- Isabelle symbols and fonts;
wenzelm [Mon, 24 Jan 2011 21:30:33 +0100] rev 41628
improved README -- Isabelle symbols and fonts;
Mon, 24 Jan 2011 15:39:42 +0100 delete compiled .elc files to improve portability on Linux, notably for GNU Emacs 23.1.x instead of 23.2.x;
wenzelm [Mon, 24 Jan 2011 15:39:42 +0100] rev 41627
delete compiled .elc files to improve portability on Linux, notably for GNU Emacs 23.1.x instead of 23.2.x;
Sun, 23 Jan 2011 16:29:10 +0100 do not overwrite proof-shell-quit-timeout by default (final PG 4.1 supposedly gets it right);
wenzelm [Sun, 23 Jan 2011 16:29:10 +0100] rev 41626
do not overwrite proof-shell-quit-timeout by default (final PG 4.1 supposedly gets it right);
Sun, 23 Jan 2011 13:28:10 +0100 Added tag isa2011-test2 for changeset 237328506a42
wenzelm [Sun, 23 Jan 2011 13:28:10 +0100] rev 41625
Added tag isa2011-test2 for changeset 237328506a42
Sun, 23 Jan 2011 01:03:42 +0100 Documented unused_thms
berghofe [Sun, 23 Jan 2011 01:03:42 +0100] rev 41624
Documented unused_thms
Fri, 21 Jan 2011 22:04:12 +0100 JVM/Windows: more robust treatment of unicode in file names;
wenzelm [Fri, 21 Jan 2011 22:04:12 +0100] rev 41623
JVM/Windows: more robust treatment of unicode in file names;
Fri, 21 Jan 2011 19:01:40 +0100 java/scala: default to UTF-8;
wenzelm [Fri, 21 Jan 2011 19:01:40 +0100] rev 41622
java/scala: default to UTF-8;
Fri, 21 Jan 2011 17:33:55 +0100 updated Named_Target.init;
wenzelm [Fri, 21 Jan 2011 17:33:55 +0100] rev 41621
updated Named_Target.init;
Fri, 21 Jan 2011 10:35:53 +0100 made SML/NJ happy;
wenzelm [Fri, 21 Jan 2011 10:35:53 +0100] rev 41620
made SML/NJ happy;
Thu, 20 Jan 2011 21:12:25 +0100 Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm [Thu, 20 Jan 2011 21:12:25 +0100] rev 41619
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
Wed, 19 Jan 2011 20:01:18 +0100 fixing list_to_set_comprehension simproc
bulwahn [Wed, 19 Jan 2011 20:01:18 +0100] rev 41618
fixing list_to_set_comprehension simproc
Wed, 19 Jan 2011 21:46:45 +0100 more release checks;
wenzelm [Wed, 19 Jan 2011 21:46:45 +0100] rev 41617
more release checks;
Wed, 19 Jan 2011 21:45:50 +0100 potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
wenzelm [Wed, 19 Jan 2011 21:45:50 +0100] rev 41616
potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);
Wed, 19 Jan 2011 21:01:37 +0100 clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;
wenzelm [Wed, 19 Jan 2011 21:01:37 +0100] rev 41615
clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;
Wed, 19 Jan 2011 21:00:16 +0100 added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
wenzelm [Wed, 19 Jan 2011 21:00:16 +0100] rev 41614
added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
Wed, 19 Jan 2011 15:22:35 +0100 merged
wenzelm [Wed, 19 Jan 2011 15:22:35 +0100] rev 41613
merged
Wed, 19 Jan 2011 11:27:56 +0100 tuned;
wenzelm [Wed, 19 Jan 2011 11:27:56 +0100] rev 41612
tuned;
Wed, 19 Jan 2011 15:18:03 +0100 Cygwin: back to ProofGeneral-3.7.1.1 with XEmacs, since PG 4.x with GNU Emacs 23 is painfully slow;
wenzelm [Wed, 19 Jan 2011 15:18:03 +0100] rev 41611
Cygwin: back to ProofGeneral-3.7.1.1 with XEmacs, since PG 4.x with GNU Emacs 23 is painfully slow;
Tue, 18 Jan 2011 21:33:07 +0100 isabelle jedit as alternative;
wenzelm [Tue, 18 Jan 2011 21:33:07 +0100] rev 41610
isabelle jedit as alternative;
Tue, 18 Jan 2011 21:29:56 +0100 Apple's way of locating java;
wenzelm [Tue, 18 Jan 2011 21:29:56 +0100] rev 41609
Apple's way of locating java;
Tue, 18 Jan 2011 11:42:11 +0100 more notes on final release stage;
wenzelm [Tue, 18 Jan 2011 11:42:11 +0100] rev 41608
more notes on final release stage;
Mon, 17 Jan 2011 23:04:35 +0100 makedist: refer to isabelle-release;
wenzelm [Mon, 17 Jan 2011 23:04:35 +0100] rev 41607
makedist: refer to isabelle-release;
Mon, 17 Jan 2011 22:57:22 +0100 Added tag isa2011-test1 for changeset 7d035da21e9c
wenzelm [Mon, 17 Jan 2011 22:57:22 +0100] rev 41606
Added tag isa2011-test1 for changeset 7d035da21e9c
Mon, 17 Jan 2011 22:57:17 +0100 tuned;
wenzelm [Mon, 17 Jan 2011 22:57:17 +0100] rev 41605
tuned;
Mon, 17 Jan 2011 22:54:08 +0100 some announcement;
wenzelm [Mon, 17 Jan 2011 22:54:08 +0100] rev 41604
some announcement;
Mon, 17 Jan 2011 18:32:16 +0100 tuned;
wenzelm [Mon, 17 Jan 2011 18:32:16 +0100] rev 41603
tuned;
Mon, 17 Jan 2011 18:11:23 +0100 merged
wenzelm [Mon, 17 Jan 2011 18:11:23 +0100] rev 41602
merged
Mon, 17 Jan 2011 17:45:52 +0100 made Z3 the default SMT solver again
boehmes [Mon, 17 Jan 2011 17:45:52 +0100] rev 41601
made Z3 the default SMT solver again
Mon, 17 Jan 2011 18:10:46 +0100 some notes on final release stage;
wenzelm [Mon, 17 Jan 2011 18:10:46 +0100] rev 41600
some notes on final release stage;
Mon, 17 Jan 2011 17:27:26 +0100 isatest: run at-poly on macbroy28 for slightly more robust isatest-doc;
wenzelm [Mon, 17 Jan 2011 17:27:26 +0100] rev 41599
isatest: run at-poly on macbroy28 for slightly more robust isatest-doc;
Mon, 17 Jan 2011 16:57:24 +0100 keep Proof General 4.0 and 3.7.1.1 for now;
wenzelm [Mon, 17 Jan 2011 16:57:24 +0100] rev 41598
keep Proof General 4.0 and 3.7.1.1 for now;
Sun, 16 Jan 2011 21:10:30 +0100 tuned;
wenzelm [Sun, 16 Jan 2011 21:10:30 +0100] rev 41597
tuned;
Sun, 16 Jan 2011 21:05:10 +0100 misc updates for release;
wenzelm [Sun, 16 Jan 2011 21:05:10 +0100] rev 41596
misc updates for release;
Sun, 16 Jan 2011 20:55:48 +0100 tuned;
wenzelm [Sun, 16 Jan 2011 20:55:48 +0100] rev 41595
tuned;
Sun, 16 Jan 2011 20:54:30 +0100 misc tuning for release;
wenzelm [Sun, 16 Jan 2011 20:54:30 +0100] rev 41594
misc tuning for release;
Sun, 16 Jan 2011 19:45:42 +0100 merged
wenzelm [Sun, 16 Jan 2011 19:45:42 +0100] rev 41593
merged
Sun, 16 Jan 2011 17:21:13 +0100 Tuned show_status
berghofe [Sun, 16 Jan 2011 17:21:13 +0100] rev 41592
Tuned show_status
Sun, 16 Jan 2011 19:44:59 +0100 proper type variables with sorts;
wenzelm [Sun, 16 Jan 2011 19:44:59 +0100] rev 41591
proper type variables with sorts;
Sun, 16 Jan 2011 17:01:49 +0100 non-executable sources;
wenzelm [Sun, 16 Jan 2011 17:01:49 +0100] rev 41590
non-executable sources;
Sun, 16 Jan 2011 15:53:03 +0100 tuned headers;
wenzelm [Sun, 16 Jan 2011 15:53:03 +0100] rev 41589
tuned headers;
Sun, 16 Jan 2011 15:31:22 +0100 tuned;
wenzelm [Sun, 16 Jan 2011 15:31:22 +0100] rev 41588
tuned;
Sun, 16 Jan 2011 15:26:47 +0100 type_synonym;
wenzelm [Sun, 16 Jan 2011 15:26:47 +0100] rev 41587
type_synonym;
Sun, 16 Jan 2011 15:04:16 +0100 more standard command descriptions;
wenzelm [Sun, 16 Jan 2011 15:04:16 +0100] rev 41586
more standard command descriptions;
Sun, 16 Jan 2011 14:57:14 +0100 added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm [Sun, 16 Jan 2011 14:57:14 +0100] rev 41585
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
Sat, 15 Jan 2011 22:40:17 +0100 Replaced ad-hoc advance function by Position.advance
berghofe [Sat, 15 Jan 2011 22:40:17 +0100] rev 41584
Replaced ad-hoc advance function by Position.advance
Sat, 15 Jan 2011 21:24:15 +0100 merged
wenzelm [Sat, 15 Jan 2011 21:24:15 +0100] rev 41583
merged
Sat, 15 Jan 2011 20:05:29 +0100 experimental variant of interpretation with simultaneous definitions, plus example
haftmann [Sat, 15 Jan 2011 20:05:29 +0100] rev 41582
experimental variant of interpretation with simultaneous definitions, plus example
Sat, 15 Jan 2011 20:51:22 +0100 clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm [Sat, 15 Jan 2011 20:51:22 +0100] rev 41581
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
Sat, 15 Jan 2011 18:49:42 +0100 link HOL-Proofs/index.html, which is not reachable from regular HOL/index.html;
wenzelm [Sat, 15 Jan 2011 18:49:42 +0100] rev 41580
link HOL-Proofs/index.html, which is not reachable from regular HOL/index.html;
Sat, 15 Jan 2011 18:12:26 +0100 type_synonym;
wenzelm [Sat, 15 Jan 2011 18:12:26 +0100] rev 41579
type_synonym;
Sat, 15 Jan 2011 17:32:07 +0100 recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e;
wenzelm [Sat, 15 Jan 2011 17:32:07 +0100] rev 41578
recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e; tuned;
Sat, 15 Jan 2011 16:49:10 +0100 export Record.get_hierarchy -- external tools typically need this information;
wenzelm [Sat, 15 Jan 2011 16:49:10 +0100] rev 41577
export Record.get_hierarchy -- external tools typically need this information;
Sat, 15 Jan 2011 15:37:49 +0100 tuned;
wenzelm [Sat, 15 Jan 2011 15:37:49 +0100] rev 41576
tuned;
Sat, 15 Jan 2011 15:29:17 +0100 removed unreferenced identifiers;
wenzelm [Sat, 15 Jan 2011 15:29:17 +0100] rev 41575
removed unreferenced identifiers;
Sat, 15 Jan 2011 14:56:57 +0100 global "prems" is legacy feature;
wenzelm [Sat, 15 Jan 2011 14:56:57 +0100] rev 41574
global "prems" is legacy feature;
Sat, 15 Jan 2011 14:19:37 +0100 misc updates for release;
wenzelm [Sat, 15 Jan 2011 14:19:37 +0100] rev 41573
misc updates for release;
Sat, 15 Jan 2011 14:02:24 +0100 merged;
wenzelm [Sat, 15 Jan 2011 14:02:24 +0100] rev 41572
merged;
Sat, 15 Jan 2011 13:34:10 +0100 misc tuning for release;
wenzelm [Sat, 15 Jan 2011 13:34:10 +0100] rev 41571
misc tuning for release;
Sat, 15 Jan 2011 13:48:45 +0100 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes [Sat, 15 Jan 2011 13:48:45 +0100] rev 41570
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
Sat, 15 Jan 2011 13:41:58 +0100 Also added SPARK to test and clean targets.
berghofe [Sat, 15 Jan 2011 13:41:58 +0100] rev 41569
Also added SPARK to test and clean targets.
Sat, 15 Jan 2011 13:19:16 +0100 merged
berghofe [Sat, 15 Jan 2011 13:19:16 +0100] rev 41568
merged
Sat, 15 Jan 2011 12:49:10 +0100 Added entry for HOL-SPARK
berghofe [Sat, 15 Jan 2011 12:49:10 +0100] rev 41567
Added entry for HOL-SPARK
Sat, 15 Jan 2011 12:48:39 +0100 Added HOL-SPARK and removed old_primrec.ML
berghofe [Sat, 15 Jan 2011 12:48:39 +0100] rev 41566
Added HOL-SPARK and removed old_primrec.ML
Sat, 15 Jan 2011 12:47:52 +0100 unused_thms no longer compares propositions, since this is no longer needed
berghofe [Sat, 15 Jan 2011 12:47:52 +0100] rev 41565
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
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
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
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.
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;
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);
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";
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);
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;
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;
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
haftmann [Fri, 14 Jan 2011 17:20:36 +0100] rev 41554
adjusted mira configuration
Fri, 14 Jan 2011 16:14:51 +0100 merged
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;
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;
wenzelm [Fri, 14 Jan 2011 16:00:11 +0100] rev 41551
tuned markup;
Fri, 14 Jan 2011 15:44:47 +0100 eliminated global prems;
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;
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;
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
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
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
hoelzl [Fri, 14 Jan 2011 15:56:42 +0100] rev 41545
tuned formalization of subalgebra
Fri, 14 Jan 2011 14:21:48 +0100 introduced integral syntax
hoelzl [Fri, 14 Jan 2011 14:21:48 +0100] rev 41544
introduced integral syntax
Fri, 14 Jan 2011 14:21:26 +0100 tuned theorem order
hoelzl [Fri, 14 Jan 2011 14:21:26 +0100] rev 41543
tuned theorem order
Fri, 14 Jan 2011 13:59:06 +0100 configuration file for mira
haftmann [Fri, 14 Jan 2011 13:59:06 +0100] rev 41542
configuration file for mira
Thu, 13 Jan 2011 23:50:16 +0100 eliminated global prems;
wenzelm [Thu, 13 Jan 2011 23:50:16 +0100] rev 41541
eliminated global prems; tuned proofs;
Thu, 13 Jan 2011 21:50:13 +0100 more precise pretty printing -- to accomodate Scala message layout;
wenzelm [Thu, 13 Jan 2011 21:50:13 +0100] rev 41540
more precise pretty printing -- to accomodate Scala message layout;
Thu, 13 Jan 2011 20:54:07 +0100 less verbosity -- avoid slightly odd tracing information on warning channel;
wenzelm [Thu, 13 Jan 2011 20:54:07 +0100] rev 41539
less verbosity -- avoid slightly odd tracing information on warning channel;
Thu, 13 Jan 2011 18:00:13 +0100 updated Isabelle/jEdit limitations and workarounds;
wenzelm [Thu, 13 Jan 2011 18:00:13 +0100] rev 41538
updated Isabelle/jEdit limitations and workarounds;
Thu, 13 Jan 2011 17:39:35 +0100 full theory path enables loading parents via master directory and keeps files strictly separate;
wenzelm [Thu, 13 Jan 2011 17:39:35 +0100] rev 41537
full theory path enables loading parents via master directory and keeps files strictly separate;
Thu, 13 Jan 2011 17:34:45 +0100 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
wenzelm [Thu, 13 Jan 2011 17:34:45 +0100] rev 41536
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
Thu, 13 Jan 2011 17:30:52 +0100 clarified split_thy_path;
wenzelm [Thu, 13 Jan 2011 17:30:52 +0100] rev 41535
clarified split_thy_path;
Thu, 13 Jan 2011 17:27:52 +0100 less verbosity;
wenzelm [Thu, 13 Jan 2011 17:27:52 +0100] rev 41534
less verbosity;
Wed, 12 Jan 2011 16:04:47 -0800 proper 'domain' class instance for 'a defl, with deflation combinator
huffman [Wed, 12 Jan 2011 16:04:47 -0800] rev 41533
proper 'domain' class instance for 'a defl, with deflation combinator
Wed, 12 Jan 2011 21:57:01 +0100 documented Option.bind
krauss [Wed, 12 Jan 2011 21:57:01 +0100] rev 41532
documented Option.bind
Wed, 12 Jan 2011 21:49:04 +0100 CONTRIBUTORS
krauss [Wed, 12 Jan 2011 21:49:04 +0100] rev 41531
CONTRIBUTORS
Wed, 12 Jan 2011 17:33:47 +0100 updated keywords;
wenzelm [Wed, 12 Jan 2011 17:33:47 +0100] rev 41530
updated keywords;
Wed, 12 Jan 2011 17:19:50 +0100 eliminated global prems;
wenzelm [Wed, 12 Jan 2011 17:19:50 +0100] rev 41529
eliminated global prems;
Wed, 12 Jan 2011 17:14:27 +0100 eliminated global prems;
wenzelm [Wed, 12 Jan 2011 17:14:27 +0100] rev 41528
eliminated global prems; tuned proofs;
Wed, 12 Jan 2011 16:41:49 +0100 updated to ProofGeneral-4.x;
wenzelm [Wed, 12 Jan 2011 16:41:49 +0100] rev 41527
updated to ProofGeneral-4.x;
Wed, 12 Jan 2011 16:33:04 +0100 eliminated global prems;
wenzelm [Wed, 12 Jan 2011 16:33:04 +0100] rev 41526
eliminated global prems;
Wed, 12 Jan 2011 15:53:37 +0100 tuned proof;
wenzelm [Wed, 12 Jan 2011 15:53:37 +0100] rev 41525
tuned proof;
Wed, 12 Jan 2011 15:38:57 +0100 eliminated global prems;
wenzelm [Wed, 12 Jan 2011 15:38:57 +0100] rev 41524
eliminated global prems; tuned proofs;
Wed, 12 Jan 2011 15:22:24 +0100 compile;
wenzelm [Wed, 12 Jan 2011 15:22:24 +0100] rev 41523
compile;
Wed, 12 Jan 2011 15:15:51 +0100 more FIXMEs concerning bad catch-all exception handlers;
wenzelm [Wed, 12 Jan 2011 15:15:51 +0100] rev 41522
more FIXMEs concerning bad catch-all exception handlers;
Wed, 12 Jan 2011 15:09:26 +0100 eliminated obsolete print_sign_exn_unit;
wenzelm [Wed, 12 Jan 2011 15:09:26 +0100] rev 41521
eliminated obsolete print_sign_exn_unit;
Wed, 12 Jan 2011 15:08:21 +0100 reraise interrupts as usual;
wenzelm [Wed, 12 Jan 2011 15:08:21 +0100] rev 41520
reraise interrupts as usual;
Wed, 12 Jan 2011 15:07:29 +0100 avoid catch-all exception handler, presumably TERM was meant here;
wenzelm [Wed, 12 Jan 2011 15:07:29 +0100] rev 41519
avoid catch-all exception handler, presumably TERM was meant here;
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip