--- a/src/Doc/Datatypes/Datatypes.thy Tue Apr 28 19:09:28 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Apr 28 22:56:28 2015 +0200
@@ -1637,7 +1637,7 @@
text {* \blankline *}
lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs"
- by (cases xs) auto
+ by (cases xs) auto
subsection {* Compatibility Issues
@@ -2681,9 +2681,9 @@
*}
typedef ('d, 'a) fn = "UNIV \<Colon> ('d \<Rightarrow> 'a) set"
- by simp
-
- text {* \blankline *}
+ by simp
+
+text {* \blankline *}
setup_lifting type_definition_fn