changeset 5809 | bacf85370ce0 |
parent 5321 | f8848433d240 |
child 6070 | 032babd0120b |
--- a/src/ZF/QUniv.ML Fri Nov 06 15:48:37 1998 +0100 +++ b/src/ZF/QUniv.ML Mon Nov 09 10:58:49 1998 +0100 @@ -3,11 +3,9 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For quniv.thy. A small universe for lazy recursive types +A small universe for lazy recursive types *) -open QUniv; - (** Properties involving Transset and Sum **) val [prem1,prem2] = goalw QUniv.thy [sum_def]