src/HOL/Eisbach/Examples.thy

      print_term Q,
      print_term x,
      print_fact U\<close>)
 
 lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
-  apply match_test  -- \<open>Valid match, but not quite what we were expecting..\<close>
-  back  -- \<open>Can backtrack over matches, exploring all bindings\<close>
-  back
-  back
-  back
-  back
-  back  -- \<open>Found the other conjunction\<close>
+  apply match_test  \<comment> \<open>Valid match, but not quite what we were expecting..\<close>
+  back  \<comment> \<open>Can backtrack over matches, exploring all bindings\<close>
+  back
+  back
+  back
+  back
+  back  \<comment> \<open>Found the other conjunction\<close>
   back
   back
   back
   oops
 
 text \<open>Use matching to avoid "improper" methods\<close>
 
 lemma focus_test:
   shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
-  apply (my_spec "x :: 'a", assumption)?  -- \<open>Wrong x\<close>
+  apply (my_spec "x :: 'a", assumption)?  \<comment> \<open>Wrong x\<close>
   apply (match conclusion in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
   done
 
 
 text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>

     \<open>insert spec[where x=x, OF U],
      print_term P,
      print_term Q\<close>)
 
 lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
-  apply my_spec_guess2?  -- \<open>Fails. Note that both "P"s must match\<close>
+  apply my_spec_guess2?  \<comment> \<open>Fails. Note that both "P"s must match\<close>
   oops
 
 lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> P x \<Longrightarrow> Q x"
   apply my_spec_guess2
   apply (erule mp)

 
 
 subsection \<open>Solves combinator\<close>
 
 lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
-  apply (solves \<open>rule conjI\<close>)?  -- \<open>Doesn't solve the goal!\<close>
+  apply (solves \<open>rule conjI\<close>)?  \<comment> \<open>Doesn't solve the goal!\<close>
   apply (solves \<open>rule conjI, assumption, assumption\<close>)
   done
 
 
 subsection \<open>Demo\<close>

   apply guess_all
   apply prop_solver
   done
 
 lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow>  P z \<Longrightarrow> P y \<Longrightarrow> Q y"
-  apply (solves \<open>guess_all, prop_solver\<close>)  -- \<open>Try it without solve\<close>
+  apply (solves \<open>guess_all, prop_solver\<close>)  \<comment> \<open>Try it without solve\<close>
   done
 
 method guess_ex =
   (match conclusion in
     "\<exists>x. P (x :: 'a)" for P \<Rightarrow>