--- a/src/LCF/simpdata.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/LCF/simpdata.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: LCF/simpdata
+(* Title: LCF/simpdata
ID: $Id$
- Author: Tobias Nipkow, Cambridge University Computer Laboratory
+ Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Simplification data for LCF
@@ -8,9 +8,9 @@
val LCF_ss = FOL_ss addsimps
[minimal,
- UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm,
- not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU,
- not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF,
- not_FF_eq_UU,not_FF_eq_TT,
- COND_UU,COND_TT,COND_FF,
- surj_pairing,FST,SND];
+ UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm,
+ not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU,
+ not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF,
+ not_FF_eq_UU,not_FF_eq_TT,
+ COND_UU,COND_TT,COND_FF,
+ surj_pairing,FST,SND];