src/HOL/Code_Evaluation.thy
changeset 63161 2660ba498798
parent 62958 b41c1cb5e251
child 63806 c54a53ef1873
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -68,6 +68,19 @@
     1.4  
     1.5  subsection \<open>Tools setup and evaluation\<close>
     1.6  
     1.7 +context
     1.8 +begin
     1.9 +
    1.10 +qualified definition TERM_OF :: "'a::term_of itself"
    1.11 +where
    1.12 +  "TERM_OF = snd (Code_Evaluation.term_of :: 'a \<Rightarrow> _, TYPE('a))"
    1.13 +
    1.14 +qualified definition TERM_OF_EQUAL :: "'a::term_of itself"
    1.15 +where
    1.16 +  "TERM_OF_EQUAL = snd (\<lambda>(a::'a). (Code_Evaluation.term_of a, HOL.eq a), TYPE('a))"
    1.17 +
    1.18 +end
    1.19 +
    1.20  lemma eq_eq_TrueD:
    1.21    fixes x y :: "'a::{}"
    1.22    assumes "(x \<equiv> y) \<equiv> Trueprop True"