| changeset 14025 | d9b155757dc8 |
| parent 13688 | a0b16d42d489 |
| child 14674 | 3506a9af46fc |
--- a/src/HOL/Bali/Conform.thy Tue May 13 08:59:21 2003 +0200 +++ b/src/HOL/Bali/Conform.thy Wed May 14 10:22:09 2003 +0200 @@ -225,9 +225,9 @@ apply (unfold lconf_def) apply (induct_tac "vns") apply clarsimp -apply clarsimp +apply clarify apply (frule list_all2_lengthD) -apply clarsimp +apply (clarsimp) done @@ -308,7 +308,7 @@ apply (unfold wlconf_def) apply (induct_tac "vns") apply clarsimp -apply clarsimp +apply clarify apply (frule list_all2_lengthD) apply clarsimp done