--- a/TFL/examples/Subst/Unify1.thy Thu May 15 15:51:47 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-Unify1 = Unifier + WF1 + "NNF" +
-
-datatype 'a subst = Fail | Subst ('a list)
-
-consts
-
- "##" :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)" (infixr 50)
- R0 :: "('a set * 'a set) set"
- R1 :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
- R :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
-
-
-rules
-
- point_to_prod_def "(f ## g) x == (f x, g x)"
-
- (* finite proper subset -- should go in WF1.thy maybe *)
- R0_def "R0 == {p. fst p < snd p & finite(snd p)}"
-
- R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)"
-
- (* The termination relation for the Unify function *)
- R_def "R == inv_image (R0 ** R1)
- ((%(x,y). vars_of x Un vars_of y) ## (%x.x))"
-
-end