src/HOL/Code_Evaluation.thy
changeset 40638 6b137c96df07
parent 39567 5ee997fbe5cc
child 40883 b37dca06477f
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Nov 22 10:41:56 2010 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Nov 22 10:41:57 2010 +0100
     1.3 @@ -21,7 +21,10 @@
     1.4  definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
     1.5    "App _ _ = dummy_term"
     1.6  
     1.7 -code_datatype Const App
     1.8 +definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where
     1.9 +  "Abs _ _ _ = dummy_term"
    1.10 +
    1.11 +code_datatype Const App Abs
    1.12  
    1.13  class term_of = typerep +
    1.14    fixes term_of :: "'a \<Rightarrow> term"
    1.15 @@ -124,8 +127,8 @@
    1.16  code_type "term"
    1.17    (Eval "Term.term")
    1.18  
    1.19 -code_const Const and App
    1.20 -  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
    1.21 +code_const Const and App and Abs
    1.22 +  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))")
    1.23  
    1.24  code_const "term_of \<Colon> String.literal \<Rightarrow> term"
    1.25    (Eval "HOLogic.mk'_literal")
    1.26 @@ -184,7 +187,7 @@
    1.27    (Eval "Code'_Evaluation.tracing")
    1.28  
    1.29  
    1.30 -hide_const dummy_term App valapp
    1.31 -hide_const (open) Const termify valtermify term_of term_of_num tracing
    1.32 +hide_const dummy_term valapp
    1.33 +hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing
    1.34  
    1.35  end