author  wenzelm 
Tue, 24 Jul 2012 21:36:53 +0200  
changeset 48487  94a9650f79fb 
parent 48483  9bfb6978eb80 
child 48738  f8c1a5b9488f 
permissions  rwrr 
48487  1 
session ZF! in "." = Pure + 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

2 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

4 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

5 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

6 
ZermeloFraenkel Set Theory on top of classical FirstOrder Logic. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

7 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

8 
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

9 
*} 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

10 
options [document_graph] 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

11 
theories 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

12 
Main 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

13 
Main_ZFC 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

14 
files "document/root.tex" 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

15 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

16 
session AC = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

17 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

18 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

19 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

20 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

21 
Proofs of ACequivalences, due to Krzysztof Grabczewski. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

22 
*} 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

23 
options [document_graph] 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

24 
theories 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

25 
WO6_WO1 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

26 
WO1_WO7 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

27 
AC7_AC9 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

28 
WO1_AC 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

29 
AC15_WO6 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

30 
WO2_AC16 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

31 
AC16_WO4 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

32 
AC17_AC1 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

33 
AC18_AC19 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

34 
DC 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

35 
files "document/root.tex" "document/root.bib" 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

36 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

37 
session Coind = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

38 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

39 
Author: Jacob Frost, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

40 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

41 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

42 
Coind  A Coinduction Example. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

43 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

44 
Based upon the article 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

45 
Robin Milner and Mads Tofte, 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

46 
Coinduction in Relational Semantics, 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

47 
Theoretical Computer Science 87 (1991), pages 209220. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

48 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

49 
Written up as 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

50 
Jacob Frost, A Case Study of Co_induction in Isabelle 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

51 
Report, Computer Lab, University of Cambridge (1995). 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

52 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

53 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

54 
theories ECR 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

55 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

56 
session Constructible = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

57 
description {* Inner Models, Absoluteness and Consistency Proofs. *} 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

58 
options [document_graph] 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

59 
theories DPow_absolute AC_in_L Rank_Separation 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

60 
files "document/root.tex" "document/root.bib" 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

61 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

62 
session IMP = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

63 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

64 
Author: Heiko Loetzbeyer & Robert Sandner, TUM 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

65 
Copyright 1994 TUM 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

66 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

67 
Formalization of the denotational and operational semantics of a 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

68 
simple whilelanguage, including an equivalence proof. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

69 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

70 
The whole development essentially formalizes/transcribes 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

71 
chapters 2 and 5 of 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

72 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

73 
Glynn Winskel. The Formal Semantics of Programming Languages. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

74 
MIT Press, 1993. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

75 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

76 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

77 
theories Equiv 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

78 
files "document/root.tex" "document/root.bib" 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

79 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

80 
session Induct = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

81 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

82 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

83 
Copyright 2001 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

84 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

85 
Inductive definitions. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

86 
*} 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

87 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

88 
(** Datatypes **) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

89 
Datatypes (*sample datatypes*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

90 
Binary_Trees (*binary trees*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

91 
Term (*recursion over the list functor*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

92 
Ntree (*variablebranching trees; function demo*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

93 
Tree_Forest (*mutual recursion*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

94 
Brouwer (*Infinitebranching trees*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

95 
Mutil (*mutilated chess board*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

96 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

97 
(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

98 
finite sets*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

99 
Multiset 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

100 
Rmap (*mapping a relation over a list*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

101 
PropLog (*completeness of propositional logic*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

102 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

103 
(*two Coq examples by Christine PaulinMohring*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

104 
ListN 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

105 
Acc 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

106 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

107 
Comb (*Combinatory Logic example*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

108 
Primrec (*Primitive recursive functions*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

109 
files "document/root.tex" 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

110 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

111 
session Resid = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

112 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

113 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

114 
Copyright 1995 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

115 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

116 
Residuals  a proof of the ChurchRosser Theorem for the 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

117 
untyped lambdacalculus. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

118 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

119 
By Ole Rasmussen, following the Coq proof given in 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

120 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

121 
Gerard Huet. Residual Theory in LambdaCalculus: A Formal Development. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

122 
J. Functional Programming 4(3) 1994, 371394. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

123 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

124 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

125 
theories Confluence 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

126 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

127 
session UNITY = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

128 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

129 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

130 
Copyright 1998 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

131 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

132 
ZF/UNITY proofs. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

133 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

134 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

135 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

136 
(*Simple examples: no composition*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

137 
Mutex 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

138 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

139 
(*Basic metatheory*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

140 
Guar 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

141 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

142 
(*Prefix relation; the Allocator example*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

143 
Distributor Merge ClientImpl AllocImpl 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

144 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

145 
session ex = ZF + 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

146 
description {* 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

147 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

148 
Copyright 1993 University of Cambridge 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

149 

7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

150 
Miscellaneous examples for ZermeloFraenkel Set Theory. 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

151 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48462
diff
changeset

152 
options [document = false] 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

153 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

154 
misc 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

155 
Ring (*abstract algebra*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

156 
Commutation (*abstract ChurchRosser theory*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

157 
Primes (*GCD theory*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

158 
NatSum (*Summing integers, squares, cubes, etc.*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

159 
Ramsey (*Simple form of Ramsey's theorem*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

160 
Limit (*Inverse limit construction of domains*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

161 
BinEx (*Binary integer arithmetic*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

162 
LList CoUnit (*CoDatatypes*) 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

163 