Fri, 31 Jan 1997 13:57:33 +0100 oheimb changed handling of cont_lemmas and adm_lemmas
Wed, 29 Jan 1997 15:58:17 +0100 wenzelm fixed getplatform call;
Wed, 29 Jan 1997 15:45:40 +0100 wenzelm removed warning for unprintable chars in strings (functionality will
Wed, 29 Jan 1997 15:34:23 +0100 paulson The redeclaration of qed_spec_mp is unnecessary because it is now declared
Wed, 29 Jan 1997 15:32:18 +0100 paulson Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
Tue, 28 Jan 1997 16:21:15 +0100 wenzelm fixed problems with strange user .bashrc etc. (stty, ...);
Mon, 27 Jan 1997 15:29:39 +0100 paulson Tidied unicity theorems
Mon, 27 Jan 1997 15:06:21 +0100 paulson deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!
Mon, 27 Jan 1997 15:04:05 +0100 paulson Corrected faulty comment
Mon, 27 Jan 1997 15:01:17 +0100 paulson More news items, dating back to 1995
Mon, 27 Jan 1997 09:08:54 +0100 wenzelm *** empty log message ***
Fri, 24 Jan 1997 18:36:30 +0100 wenzelm *** empty log message ***
Fri, 24 Jan 1997 18:24:04 +0100 wenzelm *** empty log message ***
Fri, 24 Jan 1997 17:37:59 +0100 wenzelm Isabelle NEWS -- history of user-visible changes;
Fri, 24 Jan 1997 17:12:28 +0100 wenzelm changed case symbol to \<Rightarrow>;
Thu, 23 Jan 1997 18:16:12 +0100 wenzelm 'rm -f' instead of 'mv -f';
Thu, 23 Jan 1997 18:14:20 +0100 paulson Re-ordering of certificates so that session keys appear in decreasing order
Thu, 23 Jan 1997 18:13:07 +0100 paulson Cosmetic improvements
Thu, 23 Jan 1997 18:10:29 +0100 wenzelm 'rm -f' instead of 'cp -f';
Thu, 23 Jan 1997 14:37:45 +0100 wenzelm tuned;
Thu, 23 Jan 1997 14:35:15 +0100 wenzelm expand shorthand goal commands;
Thu, 23 Jan 1997 14:19:16 +0100 wenzelm added AxClasses test;
Thu, 23 Jan 1997 14:05:42 +0100 wenzelm replaces README;
Thu, 23 Jan 1997 13:57:31 +0100 wenzelm dummy file required for proper HTML generation;
Thu, 23 Jan 1997 13:56:50 +0100 wenzelm removed;
Thu, 23 Jan 1997 12:55:31 +0100 wenzelm removed \<mu> syntax;
Thu, 23 Jan 1997 12:42:07 +0100 wenzelm added symbols syntax;
Thu, 23 Jan 1997 10:40:21 +0100 wenzelm turned some consts into syntax;
Thu, 23 Jan 1997 10:35:28 +0100 paulson Mended spelling error
Thu, 23 Jan 1997 10:35:03 +0100 paulson Added sees_Spy_partsEs
Thu, 23 Jan 1997 10:34:18 +0100 paulson Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
Wed, 22 Jan 1997 18:17:36 +0100 nipkow Added warning msg when the simplifier cannot use a premise as a rewrite rule
Tue, 21 Jan 1997 11:29:28 +0100 nipkow Modified MiniML. Added W0.
Tue, 21 Jan 1997 10:58:32 +0100 paulson Simplified proofs
Tue, 21 Jan 1997 10:54:05 +0100 paulson Improved layout and updated comments
Mon, 20 Jan 1997 18:29:26 +0100 nipkow Improved text.
Mon, 20 Jan 1997 10:27:45 +0100 paulson Now requests runtimes of all theories
Mon, 20 Jan 1997 10:20:58 +0100 paulson Simplified Oops case of main theorem
Mon, 20 Jan 1997 10:18:47 +0100 paulson Documents the new command "prlim"
Fri, 17 Jan 1997 19:29:38 +0100 nipkow Added W0 and modified MiniML.
Fri, 17 Jan 1997 19:26:47 +0100 nipkow Ball_Un -> ball_Un
Fri, 17 Jan 1997 18:50:04 +0100 nipkow The new version of MiniML including "let".
Fri, 17 Jan 1997 18:35:44 +0100 nipkow Algorithm I has not been ported to the polymorphic version yet.
Fri, 17 Jan 1997 18:32:24 +0100 nipkow Updated documentation pointers.
Fri, 17 Jan 1997 18:20:22 +0100 wenzelm added gen_overwrite;
Fri, 17 Jan 1997 18:19:57 +0100 wenzelm addsimps, addeqcongs: replaced @ by gen_union;
Fri, 17 Jan 1997 16:58:59 +0100 nipkow Incorporated Larry's changes.
Fri, 17 Jan 1997 16:17:31 +0100 paulson New rewrites for bounded quantifiers
Fri, 17 Jan 1997 13:21:54 +0100 nipkow This is the old version og MiniML for the monomorphic case.
Fri, 17 Jan 1997 13:16:36 +0100 nipkow Modified some defs and shortened proofs.
Fri, 17 Jan 1997 12:49:31 +0100 paulson Now with Andy Gordon's treatment of freshness to replace newN/K
Fri, 17 Jan 1997 11:50:09 +0100 paulson Deleted the redundant theorem subset_empty_iff (subset_empty exists already)
Fri, 17 Jan 1997 11:13:18 +0100 paulson Added the prlim command
Fri, 17 Jan 1997 11:09:19 +0100 paulson New miniscoping rules for the bounded quantifiers and UN/INT operators
Fri, 17 Jan 1997 10:09:46 +0100 nipkow Got rid of Alls in List.
Fri, 17 Jan 1997 10:04:28 +0100 nipkow Got rid of Alls in favour of !x:set_of_list
Thu, 16 Jan 1997 16:53:15 +0100 wenzelm binary oprations and relations;
Thu, 16 Jan 1997 14:53:37 +0100 wenzelm added termless parameter;
Thu, 16 Jan 1997 13:44:47 +0100 wenzelm added term order;
Mon, 13 Jan 1997 18:24:40 +0100 wenzelm improved error msg;
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip