Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added Ord.order_antisym;
authorwenzelm
Sat, 05 Jun 1999 20:37:29 +0200
changeset 6791 2be411437c60
parent 6790 0a39f22f847a
child 6792 c68035d06cce
added Ord.order_antisym;
src/HOL/Calculation.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Calculation.thy	Sat Jun 05 20:34:53 1999 +0200
+++ b/src/HOL/Calculation.thy	Sat Jun 05 20:37:29 1999 +0200
@@ -7,15 +7,14 @@
 
 theory Calculation = Int:
 
-
-theorems[trans] = HOL.trans			(*  =  =  =  *)
-theorems[trans] = HOL.ssubst                    (*  =  *  *  *)
-theorems[trans] = HOL.subst[COMP swap_prems_rl]	(*  *  =  *  *)
+theorems[trans] = HOL.ssubst                    (*  =  x  x  *)
+theorems[trans] = HOL.subst[COMP swap_prems_rl]	(*  x  =  x  *)
 
 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		(*  <= <= =  *)
 
 theorems[trans] = Divides.dvd_trans		(* dvd dvd dvd *)
isabelle