summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 06 May 2012 13:58:05 +0200 | |

changeset 47872 | 1f6f519cdb32 |

parent 47871 | 861dc9184920 |

child 47873 | 1636ff4c6243 |

tuned proofs;

--- a/src/HOL/Isar_Examples/Group_Context.thy Sun May 06 13:22:37 2012 +0200 +++ b/src/HOL/Isar_Examples/Group_Context.thy Sun May 06 13:58:05 2012 +0200 @@ -55,10 +55,10 @@ finally show "x ** one = x" . qed -lemma one_equality: "e ** x = x \<Longrightarrow> one = e" +lemma one_equality: + assumes eq: "e ** x = x" + shows "one = e" proof - - fix e x - assume eq: "e ** x = x" have "one = x ** inverse x" by (simp only: right_inverse) also have "\<dots> = (e ** x) ** inverse x" @@ -72,10 +72,10 @@ finally show "one = e" . qed -lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'" +lemma inverse_equality: + assumes eq: "x' ** x = one" + shows "inverse x = x'" proof - - fix x x' - assume eq: "x' ** x = one" have "inverse x = one ** inverse x" by (simp only: left_one) also have "\<dots> = (x' ** x) ** inverse x"