changeset 19770 | be5c23ebe1eb |
parent 19564 | d3e2f532459a |
child 19922 | 984ae977f7aa |
19769:c40ce2de2020 | 19770:be5c23ebe1eb |
---|---|
15 |
15 |
16 |
16 |
17 |
17 |
18 structure FundefDatatype : FUNDEF_DATATYPE = |
18 structure FundefDatatype : FUNDEF_DATATYPE = |
19 struct |
19 struct |
20 |
|
20 |
21 |
21 fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) |
22 fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) |
22 fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) |
23 fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) |
23 |
24 |
24 fun inst_free var inst thm = |
25 fun inst_free var inst thm = |