src/HOL/Induct/Term.thy

Added constant abs.

(*  Title:      HOL/Induct/Term.thy
    ID:         $Id$
    Author:     Stefan Berghofer,  TU Muenchen
    Copyright   1998  TU Muenchen

Terms over a given alphabet -- function applications
*)

Term = Main +

datatype
  ('a, 'b) term = Var 'a
                | App 'b ((('a, 'b) term) list)


(** substitution function on terms **)

consts
  subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
  subst_term_list ::
    "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"

primrec
  "subst_term f (Var a) = f a"
  "subst_term f (App b ts) = App b (subst_term_list f ts)"

  "subst_term_list f [] = []"
  "subst_term_list f (t # ts) =
     subst_term f t # subst_term_list f ts"

end