Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Fun1.thy
changeset 3327 9b8e638f8602
parent 3323 194ae2e0c193
child 4721 c8a8482a8124
equal deleted inserted replaced
3326:930c9bed5a09 3327:9b8e638f8602 
    10 
    10 
    11 *)
 
    11 *)
 
    12 
    12 
    13 Fun1 = Pcpo +
 
    13 Fun1 = Pcpo +
 
    14 
    14 
       
    15 instance flat<chfin (flat_imp_chain_finite)
 
       
    16 
    15 (* to make << defineable: *)
 
    17 (* to make << defineable: *)
 
    16 instance fun  :: (term,sq_ord)sq_ord
 
    18 instance fun  :: (term,sq_ord)sq_ord
 
    17 
    19 
    18 defs
 
    20 defs
 
    19   less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
    21   less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"
isabelle