author | paulson |
Sat, 10 Jan 1998 17:59:32 +0100 | |
changeset 4552 | bb8ff763c93d |
parent 3323 | 194ae2e0c193 |
child 5068 | fb28eaa07e01 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Discrete0.ML ID: $Id$ Author: Tobias Nipkow Copyright 1997 TUM Proves that 'a discr is a po *) goalw thy [less_discr_def] "(x::('a::term)discr) << x"; by (rtac refl 1); qed "less_discr_refl"; goalw thy [less_discr_def] "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x << z"; by (etac trans 1); by (assume_tac 1); qed "less_discr_trans"; goalw thy [less_discr_def] "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y"; by (assume_tac 1); qed "less_discr_antisym";