equal
deleted
inserted
replaced
189 val replicate_app_Cons_same = thm "replicate_app_Cons_same"; |
189 val replicate_app_Cons_same = thm "replicate_app_Cons_same"; |
190 val rev_append = thm "rev_append"; |
190 val rev_append = thm "rev_append"; |
191 val rev_concat = thm "rev_concat"; |
191 val rev_concat = thm "rev_concat"; |
192 val rev_drop = thm "rev_drop"; |
192 val rev_drop = thm "rev_drop"; |
193 val rev_exhaust = thm "rev_exhaust"; |
193 val rev_exhaust = thm "rev_exhaust"; |
194 val rev_exhaust_aux = thm "rev_exhaust_aux"; |
|
195 val rev_induct = thm "rev_induct"; |
194 val rev_induct = thm "rev_induct"; |
196 val rev_is_Nil_conv = thm "rev_is_Nil_conv"; |
195 val rev_is_Nil_conv = thm "rev_is_Nil_conv"; |
197 val rev_is_rev_conv = thm "rev_is_rev_conv"; |
196 val rev_is_rev_conv = thm "rev_is_rev_conv"; |
198 val rev_map = thm "rev_map"; |
197 val rev_map = thm "rev_map"; |
199 val rev_replicate = thm "rev_replicate"; |
198 val rev_replicate = thm "rev_replicate"; |