# 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: