equal
deleted
inserted
replaced
1 (* Title: HOLCF/fun1.thy |
1 (* Title: HOLCF/Fun1.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 |
6 |
12 |
12 |
13 Fun1 = Pcpo + |
13 Fun1 = Pcpo + |
14 |
14 |
15 (* default class is still term *) |
15 (* default class is still term *) |
16 |
16 |
17 consts |
|
18 less_fun :: "['a=>'b::po,'a=>'b] => bool" |
|
19 |
|
20 defs |
17 defs |
21 (* definition of the ordering less_fun *) |
18 (* definition of the ordering less_fun *) |
22 (* in fun1.ML it is proved that less_fun is a po *) |
19 (* in fun1.ML it is proved that less_fun is a po *) |
23 |
20 |
24 less_fun_def "less_fun f1 f2 == ! x. f1(x) << f2(x)" |
21 less_fun_def "less == (%f1 f2.!x. f1 x << f2 x)" |
25 |
22 |
26 end |
23 end |
27 |
24 |
28 |
25 |
29 |
26 |