src/HOL/MiniML/Type.thy
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