summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Renamed insert_kbrl to insert_tagged_brl and exported it. Now
subgoals_of_brl calls nprems_of, which is faster than length o prems_of.

Modified proofs for new claset primitives. The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

Modified proofs for new claset primitives. The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

Recoded addSIs, etc., so that nets are built incrementally
instead of from scratch each time. The old approach used excessive time (>1
sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset
includes all record fields. joinrules no longer sorts the rules on number of
subgoals, since it does not see the full set of them; instead the number of
subgoals modifies the priority.

updated version

Simple updates for compatibility with KG

Simplified, removing needless theorems about lambda.

Tue, 25 Apr 1995 10:56:49 +0200
Now loads the theory "Let". Could add it to FOL, but this appears to

Now loads the theory "Let". Could add it to FOL, but this appears to
be incompatible with CCL.

HOL.thy:
"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.
let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)
Set.thy:
UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.
Prod.thy:
Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.
Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:
idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.
There is one more point where patterns are now allowed but don't make sense:
{e | idts . P}
where idts is the list of local variables.
Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.