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" |