use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
authorhuffman
Wed Sep 08 16:10:49 2010 -0700 (2010-09-08)
changeset 445355e681762d538
parent 44534 002b43117115
child 44536 534d7ee2644a
child 44537 c10485a6a7af
child 44540 968115499161
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
src/HOL/Hoare_Parallel/OG_Hoare.thy
     1.1 --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Fri Aug 26 10:38:29 2011 -0700
     1.2 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Sep 08 16:10:49 2010 -0700
     1.3 @@ -436,10 +436,10 @@
     1.4  apply(rule TrueI)+
     1.5  --{* Parallel *}     
     1.6        apply(simp add: SEM_def sem_def)
     1.7 -      apply clarify
     1.8 +      apply(clarify, rename_tac x y i Ts')
     1.9        apply(frule Parallel_length_post_PStar)
    1.10        apply clarify
    1.11 -      apply(drule_tac j=xb in Parallel_Strong_Soundness)
    1.12 +      apply(drule_tac j=i in Parallel_Strong_Soundness)
    1.13           apply clarify
    1.14          apply simp
    1.15         apply force