| changeset 55414 | eab03e9cee8a |
| parent 53015 | a1119cf551e8 |
| child 56073 | 29e308b56d23 |
--- a/src/HOL/Nominal/Examples/Class2.thy Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Nominal/Examples/Class2.thy Wed Feb 12 08:35:57 2014 +0100 @@ -2881,7 +2881,7 @@ done termination -apply(relation "measure (sum_case (size\<circ>fst) (size\<circ>fst))") +apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))") apply(simp_all) done