Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
changeset 66404 7eb451adbda6
parent 66016 39d9a59d8d94
child 66453 cc19f7ca2ed6 
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Aug 12 09:19:48 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Aug 12 08:56:25 2017 +0200
@@ -25,14 +25,8 @@
   Cardinality.finite'
   Cardinality.subset'
   Cardinality.eq_set
-  Gcd_fin
-  Lcm_fin
   Euclidean_Algorithm.Gcd
   Euclidean_Algorithm.Lcm
-  "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> _"
   permutations_of_set
isabelle