equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/fun1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 |
|
7 Definition of the partial ordering for the type of all functions => (fun) |
|
8 |
|
9 REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !! |
|
10 |
|
11 *) |
|
12 |
|
13 Fun1 = Pcpo + |
|
14 |
|
15 (* default class is still term *) |
|
16 |
|
17 consts |
|
18 less_fun :: "['a=>'b::po,'a=>'b] => bool" |
|
19 |
|
20 rules |
|
21 (* definition of the ordering less_fun *) |
|
22 (* in fun1.ML it is proved that less_fun is a po *) |
|
23 |
|
24 less_fun_def "less_fun(f1,f2) == ! x. f1(x) << f2(x)" |
|
25 |
|
26 end |
|
27 |
|
28 |
|
29 |
|
30 |