added rule_attribute: ('a -> thm -> thm) -> 'a attribute;
added tag / untag attributes;
(* Title : RComplete.thy Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Description : Completeness theorems for positive reals and reals *) RComplete = Lubs + Real