# HG changeset patch # User nipkow # Date 1288811964 -3600 # Node ID d1c14898fd04e8804fea44f41b816c60c4d82869 # Parent 69930308b89615f02310323fa5260819051d2c25 cleaned up diff -r 69930308b896 -r d1c14898fd04 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Wed Nov 03 17:11:40 2010 +0100 +++ b/src/HOL/Bali/Eval.thy Wed Nov 03 20:19:24 2010 +0100 @@ -745,7 +745,7 @@ *) ML {* -bind_thm ("eval_induct_", rearrange_prems +bind_thm ("eval_induct", rearrange_prems [0,1,2,8,4,30,31,27,15,16, 17,18,19,20,21,3,5,25,26,23,6, 7,11,9,13,14,12,22,10,28, @@ -753,11 +753,6 @@ *} -lemmas eval_induct = eval_induct_ [split_format and and and and and and and and - and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and - and and - s2 (* Fin *) and and s2 (* NewC *)] - declare split_if [split del] split_if_asm [split del] option.split [split del] option.split_asm [split del] inductive_cases halloc_elim_cases: