Added theorems True_not_False and False_not_True
(for rep_datatype).
(* Title : RealAbs.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : Absolute value function for the reals
*)
RealAbs = Real +
constdefs
rabs :: real => real
"rabs r == if 0r<=r then r else -r"
end