Time Nick Message 00:38 chindy is there a standard way of limiting the set real to all reals >0 ? 07:13 pruvisto chindy: {x. x > 0} 17:26 chindy how do i specify a set of all elements of type: For example for showing total_on as an example: "total_on_nat Rel ⟷ (total_on (Nats::nat) (Rel:: nat * nat))". where i intend to show that Rel is total on Natural numbers 17:47 ammbauer chindy: use UNIV. 17:47 ammbauer "total_on_nat Rel <--> total_on UNIV (Rel::nat rel)" 17:47 ammbauer or with fancy abbreviation "total_on_nat Rel <--> total (Rel::nat rel)" 18:06 chindy so "let s = UNIV (X::real set) in" .... lets s be a set of all elements e taht are element of real ? 18:08 int-e UNIV :: real set is the set of all real numbers. 18:12 int-e note: lemma "{x. True} = UNIV" by simp 18:19 chindy ah thx 20:47 JCaesar btw, the statement 'element of real' doesn't really make sense in Isabelle/HOL… 20:48 pruvisto Well, there is the constant "ℝ", which is the set of all real numbers 20:49 pruvisto but it only makes sense as a subset of a real algebra 20:49 pruvisto e.g. you can have "ℝ :: complex" 20:49 pruvisto the set of all real numbers, viewed as a subset of the complex numbers 21:22 chindy pruvisto: thanks, but I think in my case it made sense as i had a (real, real) set and needed it to be total, which needs a set so "total_on (UNIV :: real set) relation" is probably the way to go