equal
deleted
inserted
replaced
7 |
7 |
8 UTLemmas = UTerm + Setplus + |
8 UTLemmas = UTerm + Setplus + |
9 |
9 |
10 consts |
10 consts |
11 |
11 |
12 vars_of :: "'a uterm=>'a set" |
12 vars_of :: 'a uterm=>'a set |
13 "<:" :: "['a uterm,'a uterm]=>bool" (infixl 54) |
13 "<:" :: ['a uterm,'a uterm]=>bool (infixl 54) |
14 |
14 |
15 rules (*Definitions*) |
15 rules (*Definitions*) |
16 |
16 |
17 vars_of_def "vars_of(t) == uterm_rec t (%x.{x}) (%x.{}) (%u v q r.q Un r)" |
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)" |
18 occs_def "s <: t == uterm_rec t (%x.False) (%x.False) (%u v q r.s=u | s=v | q | r)" |