src/HOL/MicroJava/J/Decl.ML
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/Decl.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Decl.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  	rtac finite_map_of 1]);
     1.5  
     1.6  val is_classI = prove_goalw thy [is_class_def]
     1.7 -"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
     1.8 +"!!G. class G C = Some c ==> is_class G C" (K [Auto_tac]);
     1.9  
    1.10  val is_classD = prove_goalw thy [is_class_def]
    1.11 -"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
    1.12 +"!!G. is_class G C ==> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
    1.13  	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);