9 |
9 |
10 structure Data = Datatype_Fun |
10 structure Data = Datatype_Fun |
11 (val thy = Univ.thy |
11 (val thy = Univ.thy |
12 val thy_name = "Data" |
12 val thy_name = "Data" |
13 val rec_specs = [("data", "univ(A Un B)", |
13 val rec_specs = [("data", "univ(A Un B)", |
14 [(["Con0"], "i",NoSyn), |
14 [(["Con0"], "i", NoSyn), |
15 (["Con1"], "i=>i",NoSyn), |
15 (["Con1"], "i=>i", NoSyn), |
16 (["Con2"], "[i,i]=>i",NoSyn), |
16 (["Con2"], "[i,i]=>i", NoSyn), |
17 (["Con3"], "[i,i,i]=>i",NoSyn)])] |
17 (["Con3"], "[i,i,i]=>i", NoSyn)])] |
18 val rec_styp = "[i,i]=>i" |
18 val rec_styp = "[i,i]=>i" |
19 val sintrs = |
19 val sintrs = |
20 ["Con0 : data(A,B)", |
20 ["Con0 : data(A,B)", |
21 "[| a: A |] ==> Con1(a) : data(A,B)", |
21 "[| a: A |] ==> Con1(a) : data(A,B)", |
22 "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", |
22 "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", |