equal
deleted
inserted
replaced
1 (* Title: HOL/Univ |
1 (* Title: HOL/Univ |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
|
6 For univ.thy |
|
7 *) |
5 *) |
8 |
|
9 open Univ; |
|
10 |
6 |
11 (** apfst -- can be used in similar type definitions **) |
7 (** apfst -- can be used in similar type definitions **) |
12 |
8 |
13 Goalw [apfst_def] "apfst f (a,b) = (f(a),b)"; |
9 Goalw [apfst_def] "apfst f (a,b) = (f(a),b)"; |
14 by (rtac split 1); |
10 by (rtac split 1); |