Fri, 31 Jan 1997 17:13:19 +0100 ex_impE was incorrectly listed as Safe
paulson [Fri, 31 Jan 1997 17:13:19 +0100] rev 2572
ex_impE was incorrectly listed as Safe
Fri, 31 Jan 1997 16:57:45 +0100 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
oheimb [Fri, 31 Jan 1997 16:57:45 +0100] rev 2571
reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
Fri, 31 Jan 1997 16:56:32 +0100 added Classlib.* and Witness.*,
oheimb [Fri, 31 Jan 1997 16:56:32 +0100] rev 2570
added Classlib.* and Witness.*, moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.* and Stream.* from HOLCF/explicit_domains to here adapted several proofs; now they work again. Hope that the following strange errors (when committing) do not matter: rlog error: RCS/Classlib.ML,v: No such file or directory rlog error: RCS/Classlib.thy,v: No such file or directory rlog error: RCS/Coind.ML,v: No such file or directory rlog error: RCS/Coind.thy,v: No such file or directory rlog error: RCS/Dagstuhl.ML,v: No such file or directory rlog error: RCS/Dagstuhl.thy,v: No such file or directory rlog error: RCS/Dlist.ML,v: No such file or directory rlog error: RCS/Dlist.thy,v: No such file or directory rlog error: RCS/Dnat.ML,v: No such file or directory rlog error: RCS/Dnat.thy,v: No such file or directory rlog error: RCS/Focus_ex.ML,v: No such file or directory rlog error: RCS/Focus_ex.thy,v: No such file or directory rlog error: RCS/Stream.ML,v: No such file or directory rlog error: RCS/Stream.thy,v: No such file or directory rlog error: RCS/Witness.ML,v: No such file or directory rlog error: RCS/Witness.thy,v: No such file or directory
Fri, 31 Jan 1997 16:51:58 +0100 moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex,
oheimb [Fri, 31 Jan 1997 16:51:58 +0100] rev 2569
moved Coind.*, Dagstuhl.*, Focus_ex.* to HOLCF/ex, marked the remaining files as obsolete (new versions in HOLCF/ex)
Fri, 31 Jan 1997 16:39:27 +0100 added def_fix_ind and def_wfix_ind for convenience
oheimb [Fri, 31 Jan 1997 16:39:27 +0100] rev 2568
added def_fix_ind and def_wfix_ind for convenience
Fri, 31 Jan 1997 15:54:00 +0100 added addloop (and also documentation of addsolver
oheimb [Fri, 31 Jan 1997 15:54:00 +0100] rev 2567
added addloop (and also documentation of addsolver
Fri, 31 Jan 1997 13:57:33 +0100 changed handling of cont_lemmas and adm_lemmas
oheimb [Fri, 31 Jan 1997 13:57:33 +0100] rev 2566
changed handling of cont_lemmas and adm_lemmas
Wed, 29 Jan 1997 15:58:17 +0100 fixed getplatform call;
wenzelm [Wed, 29 Jan 1997 15:58:17 +0100] rev 2565
fixed getplatform call;
Wed, 29 Jan 1997 15:45:40 +0100 removed warning for unprintable chars in strings (functionality will
wenzelm [Wed, 29 Jan 1997 15:45:40 +0100] rev 2564
removed warning for unprintable chars in strings (functionality will be put into administrative script);
Wed, 29 Jan 1997 15:34:23 +0100 The redeclaration of qed_spec_mp is unnecessary because it is now declared
paulson [Wed, 29 Jan 1997 15:34:23 +0100] rev 2563
The redeclaration of qed_spec_mp is unnecessary because it is now declared in HOL/thy_data.ML
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip