src/HOL/MicroJava/J/JTypeSafe.thy
changeset 54742 7a86358a3c0b
parent 51798 ad3a241def73
child 57492 74bf65a1910a
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -325,7 +325,7 @@
     1.4    apply(  fast intro: hext_trans)
     1.5  
     1.6  
     1.7 -apply( tactic prune_params_tac)
     1.8 +apply( tactic "prune_params_tac @{context}")
     1.9  -- "Level 52"
    1.10  
    1.11  -- "1 Call"