# HG changeset patch # User paulson # Date 826041017 -3600 # Node ID 53fe25620a033bf874095d4e732f0c4414bfd896 # Parent 03e727af711df2c1f7e2443031b794ede72e91f6 New documentation for examples diff -r 03e727af711d -r 53fe25620a03 src/ZF/AC/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/README.html Tue Mar 05 16:50:17 1996 +0100 @@ -0,0 +1,24 @@ + +HOL/AC + +

AC -- Equivalents of the Axiom of Choice

+ +Krzysztof Grabczewski has mechanized the first two chapters of the book + +

+

+@book{rubin&rubin,
+  author	= "Herman Rubin and Jean E. Rubin",
+  title		= "Equivalents of the Axiom of Choice, {II}",
+  publisher	= "North-Holland",
+  year		= 1985}
+
+ +

+The report +Mechanizing Set Theory, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals. +

+ +

+ +

Last modified 5 March 1996 diff -r 03e727af711d -r 53fe25620a03 src/ZF/Coind/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Coind/README.html Tue Mar 05 16:50:17 1996 +0100 @@ -0,0 +1,33 @@ + +HOL/Coind + +

Coind -- A Coinduction Example

+ +Jacob Frost has mechanized the proofs from the article + +

+

+@Article{milner-coind,
+  author	= "Robin Milner and Mads Tofte",
+  title		= "Co-induction in Relational Semantics",
+  journal	= TCS,
+  year		= 1991,
+  volume	= 87,
+  pages		= "209--220"}
+
+ +

It involves proving the consistency of the dynamic and static semantics +for a small functional language. A codatatype definition specifies values and +value environments in mutual recursion: non-well-founded values represent +recursive functions; value environments are variant functions from variables +into values. + +

+Frost's +report describes this development. +

+ +

+ +

Last modified 5 March 1996