equal
deleted
inserted
replaced
8 Candidates |
8 Candidates |
9 "~~/src/HOL/Library/DAList_Multiset" |
9 "~~/src/HOL/Library/DAList_Multiset" |
10 "~~/src/HOL/Library/RBT_Mapping" |
10 "~~/src/HOL/Library/RBT_Mapping" |
11 "~~/src/HOL/Library/RBT_Set" |
11 "~~/src/HOL/Library/RBT_Set" |
12 begin |
12 begin |
|
13 |
|
14 setup \<open> |
|
15 let |
|
16 val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory}; |
|
17 val consts = map_filter (try (curry (Axclass.param_of_inst @{theory}) |
|
18 @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos; |
|
19 in fold Code.del_eqns consts end |
|
20 \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close> |
13 |
21 |
14 (* |
22 (* |
15 The following code equations have to be deleted because they use |
23 The following code equations have to be deleted because they use |
16 lists to implement sets in the code generetor. |
24 lists to implement sets in the code generetor. |
17 *) |
25 *) |