src/HOL/MicroJava/J/WellForm.thy
changeset 14174 f3cafd2929d5
parent 14045 a34d89ce6097
child 15076 4b3d280ef06a
     1.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Fri Aug 29 13:18:45 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Fri Aug 29 15:19:02 2003 +0200
     1.3 @@ -547,7 +547,7 @@
     1.4    apply (assumption)
     1.5   apply (assumption)
     1.6  apply (clarify)
     1.7 -apply (erule_tac "x" = "Da" in allE)
     1.8 +apply (erule_tac x = "Da" in allE)
     1.9  apply (clarsimp)
    1.10   apply (simp add: map_of_map)
    1.11   apply (clarify)
    1.12 @@ -571,7 +571,7 @@
    1.13    apply (assumption)
    1.14   apply (assumption)
    1.15  apply (clarify)
    1.16 -apply (erule_tac "x" = "Da" in allE)
    1.17 +apply (erule_tac x = "Da" in allE)
    1.18  apply (clarsimp)
    1.19   apply (simp add: map_of_map)
    1.20   apply (clarify)