Nominal/Ex/ExPS7.thy
changeset 2454 9ffee4eb1ae1
parent 2436 3885dc2669f9
child 2480 ac7dff1194e8
--- a/Nominal/Ex/ExPS7.thy	Sun Aug 29 12:17:25 2010 +0800
+++ b/Nominal/Ex/ExPS7.thy	Sun Aug 29 13:36:03 2010 +0800
@@ -1,6 +1,5 @@
-
 theory ExPS7
-imports "../NewParser"
+imports "../Nominal2"
 begin
 
 (* example 7 from Peter Sewell's bestiary *)