author | clasohm |
Fri, 03 Mar 1995 12:04:45 +0100 | |
changeset 925 | 15539deb6863 |
parent 190 | 4ae10fc91cba |
child 1461 | 6bcb44e4d6e5 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: LCF/simpdata |
2 |
ID: $Id$ |
|
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, |
0 | 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]; |