1 (* Title: LCF/simpdata |
1 (* Title: LCF/simpdata |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Simplification data for LCF |
6 Simplification data for LCF |
7 *) |
7 *) |
8 |
8 |
9 val LCF_ss = FOL_ss addsimps |
9 val LCF_ss = FOL_ss addsimps |
10 [minimal, |
10 [minimal, |
11 UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm, |
11 UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm, |
12 not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU, |
12 not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU, |
13 not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF, |
13 not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF, |
14 not_FF_eq_UU,not_FF_eq_TT, |
14 not_FF_eq_UU,not_FF_eq_TT, |
15 COND_UU,COND_TT,COND_FF, |
15 COND_UU,COND_TT,COND_FF, |
16 surj_pairing,FST,SND]; |
16 surj_pairing,FST,SND]; |