wenzelm [Fri, 06 Nov 1998 14:04:54 +0100] rev 5807
spell check;
wenzelm [Fri, 06 Nov 1998 13:58:59 +0100] rev 5806
tuned;
mueller [Fri, 06 Nov 1998 13:42:13 +0100] rev 5805
added mailing list, removed mirrors;
paulson [Fri, 06 Nov 1998 13:20:29 +0100] rev 5804
Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
mueller [Thu, 05 Nov 1998 15:33:27 +0100] rev 5803
made more generic;
nipkow [Thu, 05 Nov 1998 14:05:57 +0100] rev 5802
Shortened names and added new thm.
paulson [Wed, 04 Nov 1998 13:00:15 +0100] rev 5801
Some streamlining of text.
Theory library is now assumed to be LOCAL and not at TUM.
wenzelm [Tue, 03 Nov 1998 17:44:16 +0100] rev 5800
tuned;
wenzelm [Tue, 03 Nov 1998 09:57:53 +0100] rev 5799
tuned width of pics;
wenzelm [Tue, 03 Nov 1998 09:47:49 +0100] rev 5798
tuned;
wenzelm [Mon, 02 Nov 1998 22:18:35 +0100] rev 5797
oops;
wenzelm [Mon, 02 Nov 1998 22:16:49 +0100] rev 5796
tuned pics;
wenzelm [Mon, 02 Nov 1998 22:00:12 +0100] rev 5795
made weblint happy;
wenzelm [Mon, 02 Nov 1998 21:57:49 +0100] rev 5794
oops;
wenzelm [Mon, 02 Nov 1998 21:36:48 +0100] rev 5793
Id;
wenzelm [Mon, 02 Nov 1998 21:34:40 +0100] rev 5792
tuned;
fixed links;
wenzelm [Mon, 02 Nov 1998 21:22:03 +0100] rev 5791
tuned;
wenzelm [Mon, 02 Nov 1998 21:15:55 +0100] rev 5790
main Isabelle page;
nipkow [Mon, 02 Nov 1998 18:02:53 +0100] rev 5789
New example
paulson [Mon, 02 Nov 1998 15:31:29 +0100] rev 5788
Domain r, Range r replace fst``r, snd``r
paulson [Mon, 02 Nov 1998 12:36:16 +0100] rev 5787
increased precedence of unary minus from 80 to 100
requires a similar increase for %# and %%#
paulson [Mon, 02 Nov 1998 12:35:14 +0100] rev 5786
increased precedence of unary minus from 80 to 100
paulson [Sat, 31 Oct 1998 12:46:21 +0100] rev 5785
Charpentier laws
paulson [Sat, 31 Oct 1998 12:45:25 +0100] rev 5784
the Increasing operator
paulson [Sat, 31 Oct 1998 12:43:56 +0100] rev 5783
no need for int_0
paulson [Sat, 31 Oct 1998 12:42:34 +0100] rev 5782
locales now implicitly quantify over free variables
wenzelm [Fri, 30 Oct 1998 15:59:51 +0100] rev 5781
tuned current_goals_markers;
paulson [Fri, 30 Oct 1998 10:45:08 +0100] rev 5780
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
paulson [Fri, 30 Oct 1998 10:43:12 +0100] rev 5779
Explicit (and improved) simprules for binary arithmetic.
New default simprules to eliminate (int 0) and (z + - w)
wenzelm [Thu, 29 Oct 1998 15:06:21 +0100] rev 5778
*** empty log message ***
wenzelm [Thu, 29 Oct 1998 15:06:10 +0100] rev 5777
shyps note for prim. rules;
wenzelm [Thu, 29 Oct 1998 15:05:42 +0100] rev 5776
tuned;
wenzelm [Thu, 29 Oct 1998 14:32:43 +0100] rev 5775
tuned current_goals_markers semantics to avoid empty lines;
paulson [Thu, 29 Oct 1998 12:42:33 +0100] rev 5774
tidied
paulson [Thu, 29 Oct 1998 12:41:45 +0100] rev 5773
auto update
nipkow [Wed, 28 Oct 1998 13:25:09 +0100] rev 5772
Some more proofs.
nipkow [Wed, 28 Oct 1998 11:25:38 +0100] rev 5771
added nat_diff_split and a few lemmas in Trancl.
wenzelm [Mon, 26 Oct 1998 13:05:08 +0100] rev 5770
ML_SYSTEM=polyml-3.1;
wenzelm [Sun, 25 Oct 1998 12:33:27 +0100] rev 5769
tuned checklist;
wenzelm [Sat, 24 Oct 1998 21:25:43 +0200] rev 5768
official release;
wenzelm [Sat, 24 Oct 1998 21:21:21 +0200] rev 5767
ML_SYSTEM factory default;
wenzelm [Sat, 24 Oct 1998 20:28:03 +0200] rev 5766
*** empty log message ***
wenzelm [Sat, 24 Oct 1998 20:24:33 +0200] rev 5765
tuned;
wenzelm [Sat, 24 Oct 1998 20:22:45 +0200] rev 5764
records;
tuned datatype, inductive, primrec;
wenzelm [Sat, 24 Oct 1998 17:16:20 +0200] rev 5763
*** empty log message ***
berghofe [Fri, 23 Oct 1998 22:37:15 +0200] rev 5762
Added theorem bool_induct (for rep_datatype).
berghofe [Fri, 23 Oct 1998 22:36:49 +0200] rev 5761
Added theorem unit_induct (for rep_datatype).
berghofe [Fri, 23 Oct 1998 22:36:15 +0200] rev 5760
Added theorems True_not_False and False_not_True
(for rep_datatype).