# HG changeset patch
# User blanchet
# Date 1458650690 -3600
# Node ID 9d706e37ddab492223d799cba3cc0101f0fb038c
# Parent  84a302ab9147c2260c5fb0c265d1914cca2b5f48
tuned whitespace

diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Corec_Examples/LFilter.thy
--- 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)
diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Corec_Examples/Stream_Processor.thy
--- 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)
diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Corec_Examples/Tests/Merge_Poly.thy
--- 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
 
diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Corec_Examples/Tests/Misc_Poly.thy
--- 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
diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Tools/BNF/bnf_axiomatization.ML
--- 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));
 
diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- 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
diff -r 84a302ab9147 -r 9d706e37ddab src/HOL/Tools/BNF/bnf_lfp.ML
--- 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,