src/HOL/Subst/UTLemmas.thy
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1476 608483c2122a
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
     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