Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Subst/UTLemmas.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1476 608483c2122a
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

(*  Title:      Substitutions/utermlemmas.thy
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Additional definitions for uterms that are not part of the basic inductive definition.
*)

UTLemmas = UTerm + Setplus +

consts

  vars_of       ::   'a uterm=>'a set
  "<:"          ::   ['a uterm,'a uterm]=>bool   (infixl 54) 

rules  (*Definitions*)

  vars_of_def   "vars_of(t) == uterm_rec t (%x.{x}) (%x.{}) (%u v q r.q Un r)"
  occs_def      "s <: t == uterm_rec t (%x.False) (%x.False) (%u v q r.s=u | s=v | q | r)"

end
isabelle