Mon, 30 Sep 2002 16:27:38 +0200 - additional congruence rules for boolean operators
berghofe [Mon, 30 Sep 2002 16:27:38 +0200] rev 13602
- additional congruence rules for boolean operators - additional rewrite rules for exI / exE
Mon, 30 Sep 2002 16:14:02 +0200 Adapted to new simplifier.
berghofe [Mon, 30 Sep 2002 16:14:02 +0200] rev 13601
Adapted to new simplifier.
Mon, 30 Sep 2002 16:12:16 +0200 Removed nRS again because extract_rews now takes care of preserving names.
berghofe [Mon, 30 Sep 2002 16:12:16 +0200] rev 13600
Removed nRS again because extract_rews now takes care of preserving names.
Mon, 30 Sep 2002 16:10:32 +0200 Added elim_vars to preprocessor.
berghofe [Mon, 30 Sep 2002 16:10:32 +0200] rev 13599
Added elim_vars to preprocessor.
Mon, 30 Sep 2002 16:09:05 +0200 Fixed problem with induct_conj_curry: variable C should have type prop.
berghofe [Mon, 30 Sep 2002 16:09:05 +0200] rev 13598
Fixed problem with induct_conj_curry: variable C should have type prop.
Mon, 30 Sep 2002 15:45:11 +0200 fixes !!-bound vars in induction statement automatically
nipkow [Mon, 30 Sep 2002 15:45:11 +0200] rev 13597
fixes !!-bound vars in induction statement automatically
Mon, 30 Sep 2002 15:44:21 +0200 modified induct method
nipkow [Mon, 30 Sep 2002 15:44:21 +0200] rev 13596
modified induct method
Fri, 27 Sep 2002 16:44:50 +0200 Proof tidying
paulson [Fri, 27 Sep 2002 16:44:50 +0200] rev 13595
Proof tidying
Fri, 27 Sep 2002 13:24:29 +0200 Isar experiments, etc.
paulson [Fri, 27 Sep 2002 13:24:29 +0200] rev 13594
Isar experiments, etc.
Fri, 27 Sep 2002 10:36:21 +0200 Tidied. New Pi-theorem.
paulson [Fri, 27 Sep 2002 10:36:21 +0200] rev 13593
Tidied. New Pi-theorem.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip