author | haftmann |
Sat, 05 Apr 2014 11:37:00 +0200 | |
changeset 56420 | b266e7a86485 |
parent 48985 | src/Doc/ProgProve/MyList.thy@5386df44a037 |
permissions | -rw-r--r-- |
theory MyList imports Main begin datatype 'a list = Nil | Cons 'a "'a list" fun app :: "'a list => 'a list => 'a list" where "app Nil ys = ys" | "app (Cons x xs) ys = Cons x (app xs ys)" fun rev :: "'a list => 'a list" where "rev Nil = Nil" | "rev (Cons x xs) = app (rev xs) (Cons x Nil)" value "rev(Cons True (Cons False Nil))" end