HOL/ROOT/HOL_dup_cs: removed as obsolete
HOL/ROOT: now passes "classical" to Classical_Fun
HOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac
(* Title: Substitutions/setplus.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Minor additions to HOL's set theory
*)
Setplus = Set +
rules
ssubset_def "A < B == A <= B & ~ A=B"
end