prefer formal comments;
authorwenzelm
Sun Jan 07 22:15:54 2018 +0100 (18 months ago)
changeset 673697360fe6bb423
parent 67368 e9bee1ddfe19
child 67370 86aa6e2abee1
prefer formal comments;
src/Doc/Isar_Ref/Synopsis.thy
src/HOL/Computational_Algebra/Polynomial.thy
src/HOL/Data_Structures/AA_Set.thy
src/HOL/HOLCF/IOA/ABP/Spec.thy
src/HOL/Nitpick_Examples/Hotel_Nits.thy
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Sun Jan 07 21:32:21 2018 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Sun Jan 07 22:15:54 2018 +0100
     1.3 @@ -952,10 +952,10 @@
     1.4  notepad
     1.5  begin
     1.6    assume r:
     1.7 -    "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  (* assumptions *)
     1.8 -      (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 1 *)
     1.9 -      (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 2 *)
    1.10 -      R  (* main conclusion *)"
    1.11 +    "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  \<comment> \<open>assumptions\<close>
    1.12 +      (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  \<comment> \<open>case 1\<close>
    1.13 +      (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  \<comment> \<open>case 2\<close>
    1.14 +      R  \<comment> \<open>main conclusion\<close>"
    1.15  
    1.16    have A\<^sub>1 and A\<^sub>2 \<proof>
    1.17    then have R
     2.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Jan 07 21:32:21 2018 +0100
     2.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Jan 07 22:15:54 2018 +0100
     2.3 @@ -2893,7 +2893,7 @@
     2.4    where
     2.5      "divide_poly_main lc q r d dr (Suc n) =
     2.6        (let cr = coeff r dr; a = cr div lc; mon = monom a n in
     2.7 -        if False \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
     2.8 +        if False \<or> a * lc = cr then \<comment> \<open>\<open>False \<or>\<close> is only because of problem in function-package\<close>
     2.9            divide_poly_main
    2.10              lc
    2.11              (q + mon)
     3.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Sun Jan 07 21:32:21 2018 +0100
     3.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Sun Jan 07 22:15:54 2018 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
     3.6  "split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
     3.7 -   (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
     3.8 +   (if lva = lvb \<and> lvb = lvc \<comment> \<open>\<open>lva = lvc\<close> suffices\<close>
     3.9      then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
    3.10      else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
    3.11  "split t = t"
     4.1 --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Jan 07 21:32:21 2018 +0100
     4.2 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Sun Jan 07 22:15:54 2018 +0100
     4.3 @@ -22,7 +22,7 @@
     4.4          in
     4.5          case fst(snd(tr))
     4.6          of
     4.7 -        Next =>  t=s |            (* Note that there is condition as in Sender *)
     4.8 +        Next =>  t=s |           \<comment> \<open>Note that there is condition as in Sender\<close>
     4.9          S_msg(m) => t = s@[m]  |
    4.10          R_msg(m) => s = (m#t)  |
    4.11          S_pkt(pkt) => False |
     5.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Jan 07 21:32:21 2018 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Jan 07 22:15:54 2018 +0100
     5.3 @@ -44,7 +44,7 @@
     5.4  "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
     5.5   s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
     5.6     roomk := (roomk s)(r := k'),
     5.7 -   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} (* \<and> k' = currk s r *)
     5.8 +   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<comment> \<open>\<open>\<and> k' = currk s r\<close>\<close>
     5.9                           \<or> safe s r)\<rparr> \<in> reach" |
    5.10  exit_room:
    5.11  "\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
     6.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 07 21:32:21 2018 +0100
     6.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 07 22:15:54 2018 +0100
     6.3 @@ -725,7 +725,7 @@
     6.4            Some x \<Rightarrow> Some x
     6.5        | None \<Rightarrow> full_exhaustive_class.full_exhaustive
     6.6            (\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
     6.7 -          (min (i - 1) 8) (* generate at most 8 bits *)
     6.8 +          (min (i - 1) 8) \<comment> \<open>generate at most 8 bits\<close>
     6.9        else None)"
    6.10  
    6.11  instance ..