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

author | wenzelm |

Wed, 30 Jun 1999 16:00:06 +0200 | |

changeset 6863 | 6c8bf18f9da9 |

parent 6862 | f80091bdc992 |

child 6864 | 32b5d68196d2 |

antisym first;

--- a/src/HOL/Calculation.thy Wed Jun 30 13:42:47 1999 +0200 +++ b/src/HOL/Calculation.thy Wed Jun 30 16:00:06 1999 +0200 @@ -7,22 +7,22 @@ theory Calculation = Int:; +theorems [trans] = Ord.order_antisym; (* <= <= = *) theorems [trans] = Ord.order_trans; (* <= <= <= *) theorems [trans] = Ord.order_less_trans; (* < < < *) theorems [trans] = Ord.order_le_less_trans; (* <= < < *) theorems [trans] = Ord.order_less_le_trans; (* < <= < *) -theorems [trans] = Ord.order_antisym; (* <= <= = *) -theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; +theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) by (rule HOL.subst[with y z]); -theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; +theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) by (rule HOL.ssubst[with x y]); -theorem [trans]: "[| x < y; y = z |] ==> x < z"; +theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) by (rule HOL.subst[with y z]); -theorem [trans]: "[| x = y; y < z |] ==> x < z"; +theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) by (rule HOL.ssubst[with x y]); theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *)