src/HOL/HoareParallel/RG_Examples.thy
changeset 13103 66659a4b16f6
parent 13099 4bb592cdde0e
child 13187 e5434b822a96
     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Sat May 04 15:47:21 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon May 06 09:42:20 2002 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  header {* \section{Examples} *}
     1.6  
     1.7  theory RG_Examples = RG_Syntax:
     1.8 @@ -340,12 +339,7 @@
     1.9         apply simp+
    1.10       apply(erule_tac x=j in allE)
    1.11       apply force
    1.12 -    apply simp
    1.13 -    apply clarify
    1.14 -    apply(rule conjI)
    1.15 -     apply clarify  
    1.16 -     apply simp
    1.17 -     apply(erule not_sym)
    1.18 +    apply clarsimp
    1.19      apply force
    1.20  apply force+
    1.21  done