src/HOL/ex/Executable_Relation.thy
Thu, 02 Feb 2012 10:12:11 +0100 bulwahn adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
less more (0) tip