| changeset 20503 | 503ac4c5ef91 |
| parent 20374 | 01b711328990 |
| child 20564 | 6857bd9f1a79 |
--- a/src/HOL/ex/ReflectionEx.thy Mon Sep 11 14:35:30 2006 +0200 +++ b/src/HOL/ex/ReflectionEx.thy Mon Sep 11 21:35:19 2006 +0200 @@ -173,7 +173,7 @@ "lin_mul t = (\<lambda> i. Mul i t)" lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)" -by (induct t fixing: i rule: lin_mul.induct, auto simp add: ring_eq_simps) +by (induct t arbitrary: i rule: lin_mul.induct) (auto simp add: ring_eq_simps) consts linum:: "num \<Rightarrow> num" recdef linum "measure num_size"