--- a/Subst/Subst.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Subst/Subst.thy Wed Jun 21 15:12:40 1995 +0200
@@ -12,8 +12,8 @@
"=s=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
"<|" :: "['a uterm,('a*('a uterm)) list] => 'a uterm" (infixl 55)
- "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => \
-\ ('a*('a uterm)) list" (infixl 56)
+ "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] =>
+ ('a*('a uterm)) list" (infixl 56)
sdom :: "('a*('a uterm)) list => 'a set"
srange :: "('a*('a uterm)) list => 'a set"
@@ -22,15 +22,15 @@
subst_eq_def "r =s= s == ALL t.t <| r = t <| s"
subst_def
- "t <| al == uterm_rec(t, %x.assoc(x,Var(x),al), \
-\ %x.Const(x), \
-\ %u v q r.Comb(q,r))"
+ "t <| al == uterm_rec(t, %x.assoc(x,Var(x),al),
+ %x.Const(x),
+ %u v q r.Comb(q,r))"
comp_def "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)"
sdom_def
- "sdom(al) == alist_rec(al, {}, \
-\ %x y xs g.if(Var(x)=y, g Int Compl({x}), g Un {x}))"
+ "sdom(al) == alist_rec(al, {},
+ %x y xs g.if(Var(x)=y, g Int Compl({x}), g Un {x}))"
srange_def
"srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"