(* Title: Deriving class instances for datatypes
Author: Christian Sternagel and René Thiemann <christian.sternagel|rene.thiemann@uibk.ac.at>
Maintainer: Christian Sternagel and René Thiemann
License: LGPL
*)
section ‹Loading Existing Derive-Commands›
theory Derive
imports
"Comparator_Generator/Compare_Instances"
"Equality_Generator/Equality_Instances"
"Hash_Generator/Hash_Instances"
"Countable_Generator/Countable_Generator"
begin
text‹
just load the commands to derive comparators, equality-functions, hash-functions, and the
to show that a datatype is countable, so that now all of them are available.
are further generators available in the AFP entries Containers and Show.
›
print_derives
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland