| changeset 63731 | 9f906a2eb0e7 |
| child 69597 | ff784d5a5bfb |
| 63730:75f7a77e53bb | 63731:9f906a2eb0e7 |
|---|---|
1 theory Quickcheck_Nesting |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 ML \<open> |
|
6 let |
|
7 open BNF_FP_Def_Sugar |
|
8 open BNF_LFP_Compat |
|
9 |
|
10 val compat_plugin = Plugin_Name.declare_setup @{binding compat}; |
|
11 |
|
12 fun compat fp_sugars = |
|
13 perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars))); |
|
14 in |
|
15 Theory.setup (fp_sugars_interpretation compat_plugin compat) |
|
16 end |
|
17 \<close> |
|
18 |
|
19 end |