# HG changeset patch
# User wenzelm
# Date 1202761933 -3600
# Node ID cd89870aa92f8fd7335d5070b1620075017d71a1
# Parent  b67a225b50fd6050ce490eca926395805aa1c701
imports Main;

diff -r b67a225b50fd -r cd89870aa92f src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Mon Feb 11 21:32:12 2008 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy	Mon Feb 11 21:32:13 2008 +0100
@@ -12,7 +12,7 @@
 header{*Charpentier's Generalized Prefix Relation*}
 
 theory GenPrefix
-imports Main_ZF
+imports Main
 begin
 
 definition (*really belongs in ZF/Trancl*)
diff -r b67a225b50fd -r cd89870aa92f src/ZF/UNITY/State.thy
--- a/src/ZF/UNITY/State.thy	Mon Feb 11 21:32:12 2008 +0100
+++ b/src/ZF/UNITY/State.thy	Mon Feb 11 21:32:13 2008 +0100
@@ -11,7 +11,7 @@
 
 header{*UNITY Program States*}
 
-theory State imports Main_ZF begin
+theory State imports Main begin
 
 consts var :: i
 datatype var = Var("i \<in> list(nat)")