doc-src/ZF/ROOT.ML
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 14152 12f6f18e7afc
child 42637 381fdcab0f36
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities

(* ID:         $Id$ *)
use_thy "IFOL_examples";
use_thy "FOL_examples";
use_thy "ZF_examples";
use_thy "If";