diff -r 9e4b64c51fa1 -r 14d41b5b57b3 thys/Re.thy --- a/thys/Re.thy Wed Sep 10 12:37:43 2014 +0100 +++ b/thys/Re.thy Fri Sep 19 12:54:03 2014 +0100 @@ -1,5 +1,5 @@ -(*test*) - +(*test*) + theory Re imports "Main" begin @@ -63,6 +63,8 @@ | "\ Void : EMPTY" | "\ Char c : CHAR c" +thm Prf.intros(1) + section {* The string behind a value *} fun flat :: "val \ string"