--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Wed Jan 04 21:28:29 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Wed Jan 04 21:28:29 2017 +0100
@@ -20,64 +20,31 @@
in fold Code.del_eqns consts thy end
\<close> \<comment> \<open>drop technical stuff from \<open>Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
-(*
- The following code equations have to be deleted because they use
- lists to implement sets in the code generetor.
-*)
-
-lemma [code, code del]:
- "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
-
-lemma [code, code del]:
- "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
-
-lemma [code, code del]:
- "pred_of_set = pred_of_set" ..
-
-lemma [code, code del]:
- "Wellfounded.acc = Wellfounded.acc" ..
-
-lemma [code, code del]:
- "Cardinality.card' = Cardinality.card'" ..
-
-lemma [code, code del]:
- "Cardinality.finite' = Cardinality.finite'" ..
-
-lemma [code, code del]:
- "Cardinality.subset' = Cardinality.subset'" ..
-
-lemma [code, code del]:
- "Cardinality.eq_set = Cardinality.eq_set" ..
+text \<open>
+ The following code equations have to be deleted because they use
+ lists to implement sets in the code generetor.
+\<close>
-lemma [code, code del]:
- "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
-
-lemma [code, code del]:
- "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
-
-lemma [code, code del]:
- "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
-
-lemma [code, code del]:
- "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
-
-lemma [code, code del]:
- "(Gcd :: _ poly set \<Rightarrow> _) = Gcd" ..
-
-lemma [code, code del]:
- "(Lcm :: _ poly set \<Rightarrow> _) = Lcm" ..
-
-lemma [code, code del]:
- "Gcd_eucl = Gcd_eucl" ..
-
-lemma [code, code del]:
- "Lcm_eucl = Lcm_eucl" ..
-
-lemma [code, code del]:
- "permutations_of_set = permutations_of_set" ..
-
-lemma [code, code del]:
- "permutations_of_multiset = permutations_of_multiset" ..
+declare [[code drop:
+ Sup_pred_inst.Sup_pred
+ Inf_pred_inst.Inf_pred
+ pred_of_set
+ Wellfounded.acc
+ Cardinality.card'
+ Cardinality.finite'
+ Cardinality.subset'
+ Cardinality.eq_set
+ "Gcd :: nat set \<Rightarrow> nat"
+ "Lcm :: nat set \<Rightarrow> nat"
+ "Gcd :: int set \<Rightarrow> int"
+ "Lcm :: int set \<Rightarrow> int"
+ "Gcd :: _ poly set \<Rightarrow> _"
+ "Lcm :: _ poly set \<Rightarrow> _"
+ Euclidean_Algorithm.Gcd
+ Euclidean_Algorithm.Lcm
+ permutations_of_set
+ permutations_of_multiset
+]]
(*
If the code generation ends with an exception with the following message: