author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 15563  9e125b675253 
child 16922  2128ac2aa5db 
permissions  rwrr 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

1 

15563  2 
(* legacy ML bindings *) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

3 

15563  4 
val cpo = thm "cpo"; 
5 
val least = thm "least"; 

6 
val UU_def = thm "UU_def"; 

7 
val chfin = thm "chfin"; 

8 
val ax_flat = thm "ax_flat"; 

9 
val UU_least = thm "UU_least"; 

10 
val minimal = thm "minimal"; 

11 
val thelubE = thm "thelubE"; 

12 
val is_ub_thelub = thm "is_ub_thelub"; 

13 
val is_lub_thelub = thm "is_lub_thelub"; 

14 
val lub_range_shift = thm "lub_range_shift"; 

15 
val maxinch_is_thelub = thm "maxinch_is_thelub"; 

16 
val lub_mono = thm "lub_mono"; 

17 
val lub_equal = thm "lub_equal"; 

18 
val lub_mono2 = thm "lub_mono2"; 

19 
val lub_equal2 = thm "lub_equal2"; 

20 
val lub_mono3 = thm "lub_mono3"; 

21 
val eq_UU_iff = thm "eq_UU_iff"; 

22 
val UU_I = thm "UU_I"; 

23 
val not_less2not_eq = thm "not_less2not_eq"; 

24 
val chain_UU_I = thm "chain_UU_I"; 

25 
val chain_UU_I_inverse = thm "chain_UU_I_inverse"; 

26 
val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2"; 

27 
val notUU_I = thm "notUU_I"; 

28 
val chain_mono2 = thm "chain_mono2"; 

29 
val flat_imp_chfin = thm "flat_imp_chfin"; 

30 
val flat_eq = thm "flat_eq"; 

31 
val chfin2finch = thm "chfin2finch"; 

32 
val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma"; 

33 
val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma"; 

3326  34 

15563  35 
structure Pcpo = 
36 
struct 

37 
val thy = the_context (); 

38 
val UU_def = UU_def; 

39 
end; 