equal
deleted
inserted
replaced
105 apply(simp (no_asm) only: nullable.simps) |
105 apply(simp (no_asm) only: nullable.simps) |
106 apply(simp only:) |
106 apply(simp only:) |
107 apply(simp only: L.simps) |
107 apply(simp only: L.simps) |
108 apply(simp) |
108 apply(simp) |
109 (* SEQ case *) |
109 (* SEQ case *) |
|
110 apply(simp only: L.simps) |
|
111 apply(simp) |
110 oops |
112 oops |
111 |
113 |
112 lemma nullable_correctness: |
114 lemma nullable_correctness: |
113 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
115 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
114 apply(induct r) |
116 apply(induct r) |