--- 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
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Apr 28 19:09:28 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Apr 28 22:56:28 2015 +0200
@@ -62,7 +62,7 @@
live_nesting_bnfs: BNF_Def.bnf list,
fp_ctr_sugar: fp_ctr_sugar,
fp_bnf_sugar: fp_bnf_sugar,
- fp_co_induct_sugar: fp_co_induct_sugar};
+ fp_co_induct_sugar: fp_co_induct_sugar}
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a