--- a/src/HOL/MicroJava/DFA/Kildall.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Sat Jan 02 18:48:45 2016 +0100
@@ -348,10 +348,10 @@
r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"
in while_rule)
--- "Invariant holds initially:"
+\<comment> "Invariant holds initially:"
apply (simp add:stables_def)
--- "Invariant is preserved:"
+\<comment> "Invariant is preserved:"
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
@@ -393,16 +393,16 @@
apply (blast dest!: boundedD)
--- "Postcondition holds upon termination:"
+\<comment> "Postcondition holds upon termination:"
apply(clarsimp simp add: stables_def split_paired_all)
--- "Well-foundedness of the termination relation:"
+\<comment> "Well-foundedness of the termination relation:"
apply (rule wf_lex_prod)
apply (insert orderI [THEN acc_le_listI])
apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
apply (rule wf_finite_psubset)
--- "Loop decreases along termination relation:"
+\<comment> "Loop decreases along termination relation:"
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")