author | wenzelm |
Tue, 03 Jun 1997 16:38:58 +0200 | |
changeset 3393 | e31ac367387e |
parent 1461 | 6bcb44e4d6e5 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: LCF/simpdata |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
65 | 4 |
Copyright 1993 University of Cambridge |
0 | 5 |
|
6 |
Simplification data for LCF |
|
7 |
*) |
|
8 |
||
190
4ae10fc91cba
deleted harmful basify, which pulled rewrite rules down to base type.
nipkow
parents:
65
diff
changeset
|
9 |
val LCF_ss = FOL_ss addsimps |
4ae10fc91cba
deleted harmful basify, which pulled rewrite rules down to base type.
nipkow
parents:
65
diff
changeset
|
10 |
[minimal, |
1461 | 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, |
|
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, |
|
15 |
COND_UU,COND_TT,COND_FF, |
|
16 |
surj_pairing,FST,SND]; |