New function complete_split_rule for complete splitting of partially
splitted rules (as generated by inductive definition package).
(* Title: HOL/SetInterval.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TU Muenchen
lessThan, greaterThan, atLeast, atMost
*)
SetInterval = equalities + NatArith +
constdefs
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
"{..u(} == {x. x<u}"
atMost :: "('a::ord) => 'a set" ("(1{.._})")
"{..u} == {x. x<=u}"
greaterThan :: "('a::ord) => 'a set" ("(1{')_..})")
"{)l..} == {x. l<x}"
atLeast :: "('a::ord) => 'a set" ("(1{_..})")
"{l..} == {x. l<=x}"
end