--- a/src/ZF/UNITY/GenPrefix.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy Tue May 27 11:39:03 2003 +0200
@@ -11,7 +11,7 @@
Based on Lex/Prefix
*)
-GenPrefix = ListPlus +
+GenPrefix = Main +
consts
gen_prefix :: "[i, i] => i"
@@ -38,14 +38,6 @@
strict_prefix :: i=>i
"strict_prefix(A) == prefix(A) - id(list(A))"
- (* Probably to be moved elsewhere *)
-
- Le :: i
- "Le == {<x,y>:nat*nat. x le y}"
-
- Ge :: i
- "Ge == {<x,y>:nat*nat. y le x}"
-
syntax
(* less or equal and greater or equal over prefixes *)
pfixLe :: [i, i] => o (infixl "pfixLe" 50)