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

src/FOL/FOL.thy

changeset 12164 | 0b219d9e3384 |

parent 12160 | a5cf3ea0685d |

child 12240 | 0760eda193c4 |

equal
deleted
inserted
replaced

12163:04c98351f9af | 12164:0b219d9e3384 |
---|---|

59 by (simp only: atomize_eq induct_equal_def) |
59 by (simp only: atomize_eq induct_equal_def) |

60 |
60 |

61 lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)" |
61 lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)" |

62 by (simp add: induct_implies_def) |
62 by (simp add: induct_implies_def) |

63 |
63 |

64 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq |
64 lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq |

65 lemmas induct_rulify1 = induct_atomize [symmetric, standard] |
65 lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq |

66 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def |
66 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def |

67 |
67 |

68 hide const induct_forall induct_implies induct_equal |
68 hide const induct_forall induct_implies induct_equal |

69 |
69 |

70 |
70 |