Fri, 28 Apr 1995 11:24:32 +0200 Modified proofs for new claset primitives. The problem is that they enforce
lcp [Fri, 28 Apr 1995 11:24:32 +0200] rev 1074
Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.
Fri, 28 Apr 1995 10:57:40 +0200 Recoded addSIs, etc., so that nets are built incrementally
lcp [Fri, 28 Apr 1995 10:57:40 +0200] rev 1073
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.
Tue, 25 Apr 1995 11:14:03 +0200 updated version Isabelle94-3
lcp [Tue, 25 Apr 1995 11:14:03 +0200] rev 1072
updated version
Tue, 25 Apr 1995 11:06:52 +0200 Simple updates for compatibility with KG
lcp [Tue, 25 Apr 1995 11:06:52 +0200] rev 1071
Simple updates for compatibility with KG
Tue, 25 Apr 1995 11:01:57 +0200 Simplified, removing needless theorems about lambda.
lcp [Tue, 25 Apr 1995 11:01:57 +0200] rev 1070
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
lcp [Tue, 25 Apr 1995 10:56:49 +0200] rev 1069
Now loads the theory "Let". Could add it to FOL, but this appears to be incompatible with CCL.
Sat, 22 Apr 1995 13:25:31 +0200 HOL.thy:
nipkow [Sat, 22 Apr 1995 13:25:31 +0200] rev 1068
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.
Sat, 22 Apr 1995 12:21:41 +0200 I have modified the grammar for idts (sequences of identifiers with optional
nipkow [Sat, 22 Apr 1995 12:21:41 +0200] rev 1067
I have modified the grammar for idts (sequences of identifiers with optional type annotations). idts are generally used as in abstractions, be it lambda-abstraction or quantifiers. It now has roughly the form idts = pttrn* pttrn = idt where pttrn is a new nonterminal (type) not used anywhere else. This means that the Pure syntax for idts is in fact unchanged. The point is that the new nontermianl pttrn allows later extensions of this syntax. (See, for example, HOL/Prod.thy). The name idts is not quite accurate any longer and may become downright confusing once pttrn has been extended. Something should be done about this, in particular wrt to the manual.
Wed, 19 Apr 1995 19:15:29 +0200 Simplified proofs thanks to addss.
nipkow [Wed, 19 Apr 1995 19:15:29 +0200] rev 1066
Simplified proofs thanks to addss.
Sun, 16 Apr 1995 11:59:44 +0200 Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow [Sun, 16 Apr 1995 11:59:44 +0200] rev 1065
Fixed old bug in the simplifier. Term to be simplified now carries around its maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1 in most cases (ie no Vars), hence reasonable overhead.
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip