equal
deleted
inserted
replaced
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 1991 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 |
9 |
10 fun mk_rew_rules r = |
10 fun mk_rew_rules r = |
11 let fun basify thm = |
11 let fun basify thm = |
12 (case concl_of thm of |
12 (case concl_of thm of |
13 _$(_$t$_) => (case fastype_of([],t) of |
13 _$(_$t$_) => (case fastype_of t of |
14 Type("fun",_) => basify(thm RS ap_thm) |
14 Type("fun",_) => basify(thm RS ap_thm) |
15 | _ => thm) |
15 | _ => thm) |
16 | _ => thm) |
16 | _ => thm) |
17 in map (mk_meta_eq o basify) (atomize r) end; |
17 in map (mk_meta_eq o basify) (atomize r) end; |
18 |
18 |