--- a/src/HOL/Corec_Examples/LFilter.thy Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Corec_Examples/LFilter.thy Tue Mar 22 13:44:50 2016 +0100
@@ -55,7 +55,7 @@
show "x \<in> lset xs \<inter> {x. P x}" if "x \<in> lset (lfilter P xs)" for x using that
proof(induction ys\<equiv>"lfilter P xs" arbitrary: xs rule: llist.set_induct)
case (LCons1 x xs ys)
- from this show ?case
+ from this show ?case
apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
subgoal by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
done
@@ -94,7 +94,7 @@
apply auto
done
qed
-qed
+qed
lemma lfilter_lfilter: "lfilter P \<circ> lfilter Q = lfilter (\<lambda>x. P x \<and> Q x)"
by(rule lfilter_unique)(auto elim: llist.set_cases)
--- a/src/HOL/Corec_Examples/Stream_Processor.thy Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy Tue Mar 22 13:44:50 2016 +0100
@@ -66,7 +66,7 @@
by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
(auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
-lemma run_copy_unique:
+lemma run_copy_unique:
"(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
apply corec_unique
apply(rule ext)
--- a/src/HOL/Corec_Examples/Tests/Merge_Poly.thy Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy Tue Mar 22 13:44:50 2016 +0100
@@ -102,21 +102,21 @@
friend_of_corec h1 where
"h1 x = ACons undefined undefined" sorry
-friend_of_corec h2 where
- "h2 x = (case x of
- ACons a t \<Rightarrow> ACons a (h1 (h2 t))
+friend_of_corec h2 where
+ "h2 x = (case x of
+ ACons a t \<Rightarrow> ACons a (h1 (h2 t))
| BCons b t \<Rightarrow> BCons b (h1 (h2 t)))"
sorry
friend_of_corec h3 where
- "h3 x = (case x of
- ACons a t \<Rightarrow> ACons a (h1 (h3 t))
+ "h3 x = (case x of
+ ACons a t \<Rightarrow> ACons a (h1 (h3 t))
| BCons b t \<Rightarrow> BCons b (h1 (h3 t)))"
sorry
friend_of_corec h4 where
- "h4 x = (case x of
- ACons a t \<Rightarrow> ACons a (h1 (h4 t))
+ "h4 x = (case x of
+ ACons a t \<Rightarrow> ACons a (h1 (h4 t))
| BCons b t \<Rightarrow> BCons b (h1 (h4 t)))"
sorry
--- a/src/HOL/Corec_Examples/Tests/Misc_Poly.thy Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Corec_Examples/Tests/Misc_Poly.thy Tue Mar 22 13:44:50 2016 +0100
@@ -260,7 +260,7 @@
sorry
corec f23 where
- "f23 xh = Node undefined
+ "f23 xh = Node undefined
(if is_H1 xh then
(f23 (h_tail xh)) # (branches (h_a xh))
else if is_H1 xh then
@@ -269,7 +269,7 @@
[])"
friend_of_corec f23 where
- "f23 xh = Node undefined
+ "f23 xh = Node undefined
(if is_H1 xh then
(f23 (h_tail xh)) # (branches (h_a xh))
else if is_H1 xh then
@@ -279,7 +279,7 @@
sorry
corec f24 where
- "f24 xh =
+ "f24 xh =
(if is_H1 xh then
Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
else if is_H2 xh then
@@ -288,7 +288,7 @@
Node 0 [])"
friend_of_corec f24 :: "(('b :: {zero}) \<Rightarrow> 'b tree list, 'b, 'b \<Rightarrow> 'b tree list) h \<Rightarrow> 'b tree" where
- "f24 xh =
+ "f24 xh =
(if is_H1 xh then
Node 0 ((f24 (h_tail xh)) # (h_a xh 0))
else if is_H2 xh then
--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Tue Mar 22 13:44:50 2016 +0100
@@ -121,7 +121,7 @@
val _ =
Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
- (parse_bnf_axiomatization >>
+ (parse_bnf_axiomatization >>
(fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 22 13:44:50 2016 +0100
@@ -1455,7 +1455,7 @@
val (distincts, discIs, _, split_sels, split_sel_asms) =
case_thms_of_term lthy raw_rhs;
- val raw_code_thm =
+ val raw_code_thm =
Goal.prove_sorry lthy [] [] raw_goal
(fn {context = ctxt, prems = _} =>
mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 22 13:44:50 2016 +0100
@@ -1329,7 +1329,7 @@
val vars = Variable.add_free_names lthy goal [];
in
(Goal.prove_sorry lthy vars [] goal
- (fn {context = ctxt, prems = _} =>
+ (fn {context = ctxt, prems = _} =>
mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
Rep_inverses Abs_inverses Reps)
|> Thm.close_derivation,