equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 open Types; |
7 val te_owrE = TyEnv.mk_cases "te_owr(te,f,t):TyEnv"; |
8 |
|
9 val te_owrE = |
|
10 TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv"; |
|
11 |
8 |
12 Goal "te_app(te_owr(te,x,t),x) = t"; |
9 Goal "te_app(te_owr(te,x,t),x) = t"; |
13 by (Simp_tac 1); |
10 by (Simp_tac 1); |
14 qed "te_app_owr1"; |
11 qed "te_app_owr1"; |
15 |
12 |