Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Calculation.thy
author wenzelm
Sat, 05 Jun 1999 20:37:29 +0200
changeset 6791 2be411437c60
parent 6779 2912aff958bd
child 6862 f80091bdc992
permissions -rw-r--r--
added Ord.order_antisym;

(*  Title:      HOL/Calculation.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Setup transitivity rules for calculational proofs.
*)

theory Calculation = Int:

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 *)


end
isabelle