Wed, 19 Mar 1997 10:24:39 +0100 delete_tagged_brl just ignores non-elimination rules instead of complaining
paulson [Wed, 19 Mar 1997 10:24:39 +0100] rev 2814
delete_tagged_brl just ignores non-elimination rules instead of complaining
Wed, 19 Mar 1997 10:23:09 +0100 delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson [Wed, 19 Mar 1997 10:23:09 +0100] rev 2813
delrules now deletes ALL occurrences of a rule, since it may appear in any of the four lists.
Tue, 18 Mar 1997 18:20:52 +0100 added quit();
wenzelm [Tue, 18 Mar 1997 18:20:52 +0100] rev 2812
added quit();
Tue, 18 Mar 1997 18:20:26 +0100 asserts $ISABELLE_OUTPUT_DIR;
wenzelm [Tue, 18 Mar 1997 18:20:26 +0100] rev 2811
asserts $ISABELLE_OUTPUT_DIR;
Tue, 18 Mar 1997 18:02:19 +0100 Added wp_while.
nipkow [Tue, 18 Mar 1997 18:02:19 +0100] rev 2810
Added wp_while.
Tue, 18 Mar 1997 17:03:55 +0100 added dummy set_session;
wenzelm [Tue, 18 Mar 1997 17:03:55 +0100] rev 2809
added dummy set_session;
Tue, 18 Mar 1997 17:03:05 +0100 usedir -- build object-logic or run examples;
wenzelm [Tue, 18 Mar 1997 17:03:05 +0100] rev 2808
usedir -- build object-logic or run examples;
Tue, 18 Mar 1997 15:15:01 +0100 A more explicit prefix because gensym now generates easily predicatable
paulson [Tue, 18 Mar 1997 15:15:01 +0100] rev 2807
A more explicit prefix because gensym now generates easily predicatable identifiers
Tue, 18 Mar 1997 15:12:53 +0100 gensym no longer generates random identifiers, but just enumerates them
paulson [Tue, 18 Mar 1997 15:12:53 +0100] rev 2806
gensym no longer generates random identifiers, but just enumerates them starting from A. The random number generator was needlessly slow and caused portability problems.
Tue, 18 Mar 1997 15:11:02 +0100 Made the indentation rational
paulson [Tue, 18 Mar 1997 15:11:02 +0100] rev 2805
Made the indentation rational
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip