Nominal/Ex/Test.thy
changeset 1795 e39453c8b186
parent 1773 c0eac04ae3b4
child 2045 6800fcaafa2a
--- a/Nominal/Ex/Test.thy	Thu Apr 08 11:52:05 2010 +0200
+++ b/Nominal/Ex/Test.thy	Thu Apr 08 13:04:49 2010 +0200
@@ -1,4 +1,3 @@
-(*<*)
 theory Test
 imports "../Parser"
 begin
@@ -38,10 +37,6 @@
 | "bv8 (Bar1 v x b) = {atom v}"
 *)
 
-(* example 9 from Peter Sewell's bestiary *)
-(* run out of steam at the moment *)
-
 end
-(*>*)