--- a/src/CCL/Hered.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Hered.thy Tue Mar 29 23:27:38 2011 +0200
@@ -15,18 +15,13 @@
is. Not so useful for functions!
*}
-consts
- (*** Predicates ***)
- HTTgen :: "i set => i set"
- HTT :: "i set"
+definition HTTgen :: "i set => i set" where
+ "HTTgen(R) ==
+ {t. t=true | t=false | (EX a b. t= <a, b> & a : R & b : R) |
+ (EX f. t = lam x. f(x) & (ALL x. f(x) : R))}"
-axioms
- (*** Definitions of Hereditary Termination ***)
-
- HTTgen_def:
- "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) |
- (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}"
- HTT_def: "HTT == gfp(HTTgen)"
+definition HTT :: "i set"
+ where "HTT == gfp(HTTgen)"
subsection {* Hereditary Termination *}