equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/fun2.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Class Instance =>::(term,po)po |
|
7 Definiton of least element |
|
8 *) |
|
9 |
|
10 Fun2 = Fun1 + |
|
11 |
|
12 (* default class is still term !*) |
|
13 |
|
14 (* Witness for the above arity axiom is fun1.ML *) |
|
15 |
|
16 arities fun :: (term,po)po |
|
17 |
|
18 consts |
|
19 UU_fun :: "'a::term => 'b::pcpo" |
|
20 |
|
21 rules |
|
22 |
|
23 (* instance of << for type ['a::term => 'b::po] *) |
|
24 |
|
25 inst_fun_po "(op <<)::['a=>'b::po,'a=>'b::po ]=>bool = less_fun" |
|
26 |
|
27 (* definitions *) |
|
28 (* The least element in type 'a::term => 'b::pcpo *) |
|
29 |
|
30 UU_fun_def "UU_fun == (% x.UU)" |
|
31 |
|
32 end |
|
33 |
|
34 |
|
35 |
|
36 |
|
37 |
|
38 |
|
39 |
|
40 |