# HG changeset patch
# User wenzelm
# Date 928607849 -7200
# Node ID 2be411437c602df7f88c95c175b8e4f8e0df7742
# Parent  0a39f22f847a0c442d4a92f7626e9abd2ae87b05
added Ord.order_antisym;

diff -r 0a39f22f847a -r 2be411437c60 src/HOL/Calculation.thy
--- 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 *)