Reduced priority of postfix ^* etc operators such that they are the same as
application. Eg wf r^* now needs to be written wf(r^*).
(* Title: HOL/subset.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge*)subset = Fun