Fri, 12 Oct 2001 12:13:31 +0200 removed vars_of, concls_of;
wenzelm [Fri, 12 Oct 2001 12:13:31 +0200] rev 11735
removed vars_of, concls_of; removed additional rule instantiation argument; proper enumeration of type rules; append possibilities of set and type rules (analogous to elim-intro in 'rule');
Fri, 12 Oct 2001 12:11:39 +0200 declare impE iffD1 iffD2 ad elim of Pure;
wenzelm [Fri, 12 Oct 2001 12:11:39 +0200] rev 11734
declare impE iffD1 iffD2 ad elim of Pure;
Fri, 12 Oct 2001 12:10:07 +0200 removed lookups count;
wenzelm [Fri, 12 Oct 2001 12:10:07 +0200] rev 11733
removed lookups count; always try headless rules;
Fri, 12 Oct 2001 12:09:38 +0200 added make_thm (sort-of);
wenzelm [Fri, 12 Oct 2001 12:09:38 +0200] rev 11732
added make_thm (sort-of);
Fri, 12 Oct 2001 12:09:21 +0200 added trace_rules, trace;
wenzelm [Fri, 12 Oct 2001 12:09:21 +0200] rev 11731
added trace_rules, trace;
Fri, 12 Oct 2001 12:08:57 +0200 removed get_cases, get_induct;
wenzelm [Fri, 12 Oct 2001 12:08:57 +0200] rev 11730
removed get_cases, get_induct; added find_cases[ST], finde_induct[ST]; proper indexing of types;
Fri, 12 Oct 2001 12:08:04 +0200 removed read_inst', no longer export insts';
wenzelm [Fri, 12 Oct 2001 12:08:04 +0200] rev 11729
removed read_inst', no longer export insts';
Fri, 12 Oct 2001 12:07:27 +0200 fixed typid;
wenzelm [Fri, 12 Oct 2001 12:07:27 +0200] rev 11728
fixed typid;
Fri, 12 Oct 2001 12:06:54 +0200 test: use SkipProof.make_thm instead of Thm.assume;
wenzelm [Fri, 12 Oct 2001 12:06:54 +0200] rev 11727
test: use SkipProof.make_thm instead of Thm.assume;
Fri, 12 Oct 2001 12:06:23 +0200 tuned;
wenzelm [Fri, 12 Oct 2001 12:06:23 +0200] rev 11726
tuned;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip