src/HOL/MicroJava/DFA/Listn.thy
changeset 58860 fee7cfa69c50
parent 44890 22f665a2e91c
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4  done  
     1.5  
     1.6  lemma list_update_le_cong:
     1.7 -  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
     1.8 +  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]"
     1.9  apply (unfold unfold_lesub_list)
    1.10  apply (unfold Listn.le_def)
    1.11  apply (simp add: list_all2_conv_all_nth nth_list_update)
    1.12 @@ -189,12 +189,12 @@
    1.13  done 
    1.14  
    1.15  lemma Cons_in_list_Suc [iff]:
    1.16 -  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)";
    1.17 +  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)"
    1.18  apply (simp add: in_list_Suc_iff)
    1.19  done 
    1.20  
    1.21  lemma list_not_empty:
    1.22 -  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A";
    1.23 +  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A"
    1.24  apply (induct "n")
    1.25   apply simp
    1.26  apply (simp add: in_list_Suc_iff)