author | lcp |
Mon, 01 Aug 1994 17:34:57 +0200 | |
changeset 503 | 15375d7b379c |
parent 502 | 77e36960fd9e |
child 504 | a4f09493d929 |
src/ZF/ex/Data.ML | file | annotate | diff | comparison | revisions |
--- a/src/ZF/ex/Data.ML Mon Aug 01 17:24:46 1994 +0200 +++ b/src/ZF/ex/Data.ML Mon Aug 01 17:34:57 1994 +0200 @@ -9,7 +9,7 @@ structure Data = Datatype_Fun (val thy = Univ.thy - val thy_name = "Data" + val thy_name = "Data" val rec_specs = [("data", "univ(A Un B)", [(["Con0"], "i", NoSyn), (["Con1"], "i=>i", NoSyn),