doc-src/ProgProve/Thys/MyList.thy
changeset 47302 70239da25ef6
parent 47269 29aa0c071875
--- a/doc-src/ProgProve/Thys/MyList.thy	Mon Apr 02 13:47:00 2012 +0200
+++ b/doc-src/ProgProve/Thys/MyList.thy	Mon Apr 02 20:12:10 2012 +0200
@@ -2,7 +2,7 @@
 imports Main
 begin
 
-datatype 'a list = Nil | Cons "'a" "('a list)"
+datatype 'a list = Nil | Cons 'a "'a list"
 
 fun app :: "'a list => 'a list => 'a list" where
 "app Nil ys = ys" |