| changeset 42463 | f270e3e18be5 |
| parent 42187 | b4f4ed5b8586 |
| child 45125 | c15b0faeb70a |
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Fri Apr 22 15:57:43 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sat Apr 23 13:00:19 2011 +0200 @@ -110,7 +110,7 @@ | TyAll type type ("(3\<forall><:_./ _)" [0, 10] 10) datatype binding = VarB type | TVarB type -types env = "binding list" +type_synonym env = "binding list" primrec is_TVarB :: "binding \<Rightarrow> bool" where