equal
deleted
inserted
replaced
313 apply( assumption) |
313 apply( assumption) |
314 apply( frule class_Object) |
314 apply( frule class_Object) |
315 apply( clarify) |
315 apply( clarify) |
316 apply( frule fields_rec, assumption) |
316 apply( frule fields_rec, assumption) |
317 apply( fastsimp) |
317 apply( fastsimp) |
318 apply( tactic "safe_tac HOL_cs") |
318 apply( tactic "safe_tac (put_claset HOL_cs @{context})") |
319 apply( subst fields_rec) |
319 apply( subst fields_rec) |
320 apply( assumption) |
320 apply( assumption) |
321 apply( assumption) |
321 apply( assumption) |
322 apply( simp (no_asm) split del: split_if) |
322 apply( simp (no_asm) split del: split_if) |
323 apply( rule ballI) |
323 apply( rule ballI) |