changeset 2625 | 69c1b8a493de |
parent 2525 | 477c05586286 |
child 3842 | b55686a7b22c |
--- a/src/HOL/MiniML/Type.thy Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/Type.thy Fri Feb 14 16:01:43 1997 +0100 @@ -54,6 +54,7 @@ "free_tv [] = {}" "free_tv (x#l) = (free_tv x) Un (free_tv l)" + (* executable version of free_tv: Implementation with lists *) consts free_tv_ML :: ['a::type_struct] => nat list