equal
deleted
inserted
replaced
31 |
31 |
32 |
32 |
33 subsubsection {* Class @{term term_of} *} |
33 subsubsection {* Class @{term term_of} *} |
34 |
34 |
35 class term_of = rtype + |
35 class term_of = rtype + |
36 constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> rtype" |
|
37 fixes term_of :: "'a \<Rightarrow> term" |
36 fixes term_of :: "'a \<Rightarrow> term" |
38 |
37 |
39 lemma term_of_anything: "term_of x \<equiv> t" |
38 lemma term_of_anything: "term_of x \<equiv> t" |
40 by (rule eq_reflection) (cases "term_of x", cases t, simp) |
39 by (rule eq_reflection) (cases "term_of x", cases t, simp) |
41 |
40 |