author | paulson |
Wed, 23 Apr 1997 11:00:48 +0200 | |
changeset 3017 | 84c2178db936 |
parent 2640 | ee4dfce170a0 |
child 3323 | 194ae2e0c193 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Fun1.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Definition of the partial ordering for the type of all functions => (fun) REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !! *) Fun1 = Pcpo + (* default class is still term *) defs (* definition of the ordering less_fun *) (* in fun1.ML it is proved that less_fun is a po *) less_fun_def "less == (%f1 f2.!x. f1 x << f2 x)" end