src/HOL/Subst/UTLemmas.thy
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1476 608483c2122a
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
     1 (*  Title:      Substitutions/utermlemmas.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Additional definitions for uterms that are not part of the basic inductive definition.
     6 *)
     7 
     8 UTLemmas = UTerm + Setplus +
     9 
    10 consts
    11 
    12   vars_of       ::   'a uterm=>'a set
    13   "<:"          ::   ['a uterm,'a uterm]=>bool   (infixl 54) 
    14 
    15 rules  (*Definitions*)
    16 
    17   vars_of_def   "vars_of(t) == uterm_rec t (%x.{x}) (%x.{}) (%u v q r.q Un r)"
    18   occs_def      "s <: t == uterm_rec t (%x.False) (%x.False) (%u v q r.s=u | s=v | q | r)"
    19 
    20 end