Fri, 28 Sep 2001 19:23:58 +0200 wenzelm *** empty log message ***
Fri, 28 Sep 2001 19:23:35 +0200 wenzelm prove: ``strict'' argument;
Fri, 28 Sep 2001 19:23:07 +0200 wenzelm internal thm numbering with ":" instead of "_";
Fri, 28 Sep 2001 19:22:40 +0200 wenzelm avoid handle _;
Fri, 28 Sep 2001 19:21:26 +0200 wenzelm permissive option;
Fri, 28 Sep 2001 19:19:26 +0200 wenzelm inductive: no collective atts;
Fri, 28 Sep 2001 19:18:46 +0200 wenzelm updated;
Fri, 28 Sep 2001 19:17:01 +0200 wenzelm recdef (permissive);
Fri, 28 Sep 2001 18:55:37 +0200 berghofe Tuned section about parsing and printing proof terms.
Fri, 28 Sep 2001 17:19:46 +0200 berghofe mksimps and mk_eq_True no longer raise THM exception.
Fri, 28 Sep 2001 16:45:03 +0200 berghofe Added label for section on terms.
Fri, 28 Sep 2001 16:44:27 +0200 berghofe Added documentation for proof terms.
Fri, 28 Sep 2001 16:43:50 +0200 berghofe Added TYPE to Pure grammar.
Fri, 28 Sep 2001 16:42:58 +0200 berghofe Added \ttlbrack and \ttrbrack.
Fri, 28 Sep 2001 16:42:26 +0200 berghofe Added TPHOLs2000 paper about proof terms.
Fri, 28 Sep 2001 16:15:26 +0200 wenzelm updated;
Fri, 28 Sep 2001 14:10:01 +0200 wenzelm tuned;
Fri, 28 Sep 2001 14:04:14 +0200 wenzelm tuned;
Fri, 28 Sep 2001 11:08:53 +0200 berghofe - Exchanged % and %%.
Fri, 28 Sep 2001 11:07:40 +0200 berghofe - Tuned syntax
Fri, 28 Sep 2001 11:05:37 +0200 berghofe - Exchanged % and %%
Fri, 28 Sep 2001 11:04:44 +0200 berghofe Exchanged % and %%.
Thu, 27 Sep 2001 22:30:09 +0200 wenzelm HOL: eliminated global items;
Thu, 27 Sep 2001 22:29:57 +0200 wenzelm updated;
Thu, 27 Sep 2001 22:28:16 +0200 wenzelm eliminated theories "equalities" and "mono" (made part of "Typedef",
Thu, 27 Sep 2001 22:26:00 +0200 wenzelm renamed theory "subset" to "Typedef";
Thu, 27 Sep 2001 22:25:12 +0200 wenzelm unsymbolize;
Thu, 27 Sep 2001 22:24:28 +0200 wenzelm renamed "()" to Unity;
Thu, 27 Sep 2001 22:24:09 +0200 wenzelm HOLogic.unit;
Thu, 27 Sep 2001 22:23:40 +0200 wenzelm made unit type local;
Thu, 27 Sep 2001 22:23:20 +0200 wenzelm tuned:
Thu, 27 Sep 2001 22:22:58 +0200 wenzelm renamed "()" to Unity, made local;
Thu, 27 Sep 2001 22:22:08 +0200 wenzelm added surjE;
Thu, 27 Sep 2001 18:56:39 +0200 wenzelm prepared for Isabelle2001;
Thu, 27 Sep 2001 18:46:32 +0200 wenzelm renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;
Thu, 27 Sep 2001 18:45:40 +0200 wenzelm updated;
Thu, 27 Sep 2001 18:45:23 +0200 wenzelm renamed real_of_int_eq_iff to real_of_int_inject;
Thu, 27 Sep 2001 18:44:30 +0200 wenzelm document setup;
Thu, 27 Sep 2001 18:44:12 +0200 wenzelm new-style theory;
Thu, 27 Sep 2001 18:43:40 +0200 wenzelm Square roots of primes are irrational;
Thu, 27 Sep 2001 18:43:17 +0200 wenzelm AddXIs [dvdI]; AddXEs [dvdE];
Thu, 27 Sep 2001 18:42:47 +0200 wenzelm tuned;
Thu, 27 Sep 2001 16:43:46 +0200 wenzelm tuned;
Thu, 27 Sep 2001 16:04:44 +0200 wenzelm tuned;
Thu, 27 Sep 2001 16:04:25 +0200 wenzelm AddXEs [UnI1, UnI2];
Thu, 27 Sep 2001 16:04:11 +0200 wenzelm AddXEs [disjI1, disjI2];
Thu, 27 Sep 2001 15:42:30 +0200 wenzelm ex/Hilbert_Classical.thy ex/document/root.tex;
Thu, 27 Sep 2001 15:42:08 +0200 wenzelm tuned;
Thu, 27 Sep 2001 15:42:01 +0200 wenzelm document setup;
Thu, 27 Sep 2001 15:41:48 +0200 wenzelm derive tertium-non-datur by means of Hilbert's choice operator;
Thu, 27 Sep 2001 14:35:40 +0200 wenzelm obsolete;
Thu, 27 Sep 2001 12:25:09 +0200 wenzelm updated;
Thu, 27 Sep 2001 12:24:40 +0200 wenzelm -v option;
Thu, 27 Sep 2001 12:24:19 +0200 wenzelm verbose option;
Thu, 27 Sep 2001 12:24:02 +0200 wenzelm use_dir: verbose option;
Thu, 27 Sep 2001 12:23:23 +0200 wenzelm removed option -d (now standard behaviour);
Thu, 27 Sep 2001 12:22:45 +0200 wenzelm option -v;
Wed, 26 Sep 2001 23:01:48 +0200 wenzelm activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
Wed, 26 Sep 2001 23:00:41 +0200 wenzelm updated;
Wed, 26 Sep 2001 22:26:11 +0200 wenzelm tuned order;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip