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

1 

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

3 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

4 
val refl_less = thm "refl_less"; 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

5 
val antisym_less = thm "antisym_less"; 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

6 
val trans_less = thm "trans_less"; 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

7 
val minimal2UU = thm "minimal2UU"; 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

8 
val antisym_less_inverse = thm "antisym_less_inverse"; 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

9 
val box_less = thm "box_less"; 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

10 
val po_eq_conv = thm "po_eq_conv"; 
15562  11 
val is_ub_def = thm "is_ub_def"; 
12 
val is_lub_def = thm "is_lub_def"; 

13 
val tord_def = thm "tord_def"; 

14 
val chain_def = thm "chain_def"; 

15 
val max_in_chain_def = thm "max_in_chain_def"; 

16 
val finite_chain_def = thm "finite_chain_def"; 

17 
val lub_def = thm "lub_def"; 

18 
val unique_lub = thm "unique_lub"; 

19 
val chain_mono = thm "chain_mono"; 

20 
val chain_mono3 = thm "chain_mono3"; 

21 
val chain_tord = thm "chain_tord"; 

22 
val lub = thm "lub"; 

23 
val lubI = thm "lubI"; 

24 
val thelubI = thm "thelubI"; 

25 
val lub_singleton = thm "lub_singleton"; 

26 
val is_lubD1 = thm "is_lubD1"; 

27 
val is_lub_lub = thm "is_lub_lub"; 

28 
val is_lubI = thm "is_lubI"; 

29 
val chainE = thm "chainE"; 

30 
val chainI = thm "chainI"; 

31 
val chain_shift = thm "chain_shift"; 

32 
val ub_rangeD = thm "ub_rangeD"; 

33 
val ub_rangeI = thm "ub_rangeI"; 

34 
val is_ub_lub = thm "is_ub_lub"; 

35 
val lub_finch1 = thm "lub_finch1"; 

36 
val lub_finch2 = thm "lub_finch2"; 

37 
val bin_chain = thm "bin_chain"; 

38 
val bin_chainmax = thm "bin_chainmax"; 

39 
val lub_bin_chain = thm "lub_bin_chain"; 

40 
val lub_chain_maxelem = thm "lub_chain_maxelem"; 

41 
val lub_const = thm "lub_const"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

42 

15562  43 
structure Porder = 
44 
struct 

45 
val thy = the_context (); 

46 
val is_ub_def = is_ub_def; 

47 
val is_lub_def = is_lub_def; 

48 
val tord_def = tord_def; 

49 
val chain_def = chain_def; 

50 
val max_in_chain_def = max_in_chain_def; 

51 
val finite_chain_def = finite_chain_def; 

52 
val lub_def = lub_def; 

53 
end; 