src/HOL/IMP/Sem_Equiv.thy
changeset 45015 fdac1e9880eb
parent 44890 22f665a2e91c
child 45200 1f1897ac7877
     1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:47:11 2011 +0200
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Tue Sep 20 05:48:23 2011 +0200
     1.3 @@ -83,10 +83,9 @@
     1.4           P s \<Longrightarrow> 
     1.5           d = WHILE b DO c \<Longrightarrow> 
     1.6           (WHILE b' DO c', s) \<Rightarrow> s'"  
     1.7 -proof (induct rule: big_step_induct)
     1.8 +proof (induction rule: big_step_induct)
     1.9    case (WhileTrue b s1 c s2 s3)
    1.10 -  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
    1.11 -  
    1.12 +  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
    1.13    from WhileTrue.prems
    1.14    have "P \<Turnstile> b <\<sim>> b'" by simp
    1.15    with `bval b s1` `P s1`