aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isar/IllegalEscape.thy
blob: c1d4fde56f987bc7a861e87713bb29e73c73c1e6 (plain)
1
2
3
4
5
6
7
(* See http://proofgeneral.inf.ed.ac.uk/trac/ticket/166 *)

theory IllegalEscape imports Main begin

    lemma X: "a=b ==> b=a" by simp -- "Text with \illegal escape sequence"

end