--- a/Tutorial/Tutorial2.thy Fri Jan 21 22:23:44 2011 +0100 +++ b/Tutorial/Tutorial2.thy Fri Jan 21 22:58:03 2011 +0100 @@ -24,7 +24,6 @@ type_synonym ty_ctx = "(name \<times> ty) list" - inductive valid :: "ty_ctx \<Rightarrow> bool" where