src/HOL/HoareParallel/RG_Examples.thy
changeset 13187 e5434b822a96
parent 13103 66659a4b16f6
child 13517 42efec18f5b2
     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Thu May 30 10:12:11 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Thu May 30 10:12:52 2002 +0200
     1.3 @@ -147,7 +147,10 @@
     1.4      apply simp
     1.5     apply clarify
     1.6     apply simp
     1.7 -   apply(case_tac j,simp,simp)
     1.8 +   apply(subgoal_tac "j=0")
     1.9 +    apply (rotate_tac -1)
    1.10 +    apply simp
    1.11 +   apply arith
    1.12    apply clarify
    1.13    apply(case_tac i,simp,simp)
    1.14   apply clarify   
    1.15 @@ -324,7 +327,7 @@
    1.16      apply force
    1.17     apply(rule Basic)
    1.18        apply force
    1.19 -     apply force
    1.20 +     apply fastsimp
    1.21      apply force
    1.22     apply force
    1.23    apply(rule Basic)
    1.24 @@ -340,7 +343,7 @@
    1.25       apply(erule_tac x=j in allE)
    1.26       apply force
    1.27      apply clarsimp
    1.28 -    apply force
    1.29 +    apply fastsimp
    1.30  apply force+
    1.31  done
    1.32  
    1.33 @@ -399,4 +402,4 @@
    1.34  apply force+
    1.35  done
    1.36  
    1.37 -end
    1.38 \ No newline at end of file
    1.39 +end