summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.ML

changeset 6831 | 799859f2e657 |

parent 6820 | 41d9b7bbf968 |

child 7028 | 6ea3b385e731 |

equal
deleted
inserted
replaced

6830:f8aed3706af7 | 6831:799859f2e657 |
---|---|

379 by Auto_tac; |
379 by Auto_tac; |

380 qed "Nil_is_rev_conv"; |
380 qed "Nil_is_rev_conv"; |

381 AddIffs [Nil_is_rev_conv]; |
381 AddIffs [Nil_is_rev_conv]; |

382 |
382 |

383 Goal "!ys. (rev xs = rev ys) = (xs = ys)"; |
383 Goal "!ys. (rev xs = rev ys) = (xs = ys)"; |

384 by(induct_tac "xs" 1); |
384 by (induct_tac "xs" 1); |

385 by (Force_tac 1); |
385 by (Force_tac 1); |

386 br allI 1; |
386 by (rtac allI 1); |

387 by(exhaust_tac "ys" 1); |
387 by (exhaust_tac "ys" 1); |

388 by (Asm_simp_tac 1); |
388 by (Asm_simp_tac 1); |

389 by (Force_tac 1); |
389 by (Force_tac 1); |

390 qed_spec_mp "rev_is_rev_conv"; |
390 qed_spec_mp "rev_is_rev_conv"; |

391 AddIffs [rev_is_rev_conv]; |
391 AddIffs [rev_is_rev_conv]; |

392 |
392 |