hol-mode now strips \\ instead of //

HOL-Theorem-Prover · May 20, 2014 · ca44649 · ca44649
1 parent 3fde50a
commit ca44649
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tools/hol-mode.src b/tools/hol-mode.src
@@ -293,7 +293,7 @@ how long this took."
                   end" nil nil))
 
 (defvar tactic-connective-regexp
-  "[[:space:]]*\\(THEN1\\|THENL\\|THEN\\|>>\\|>|\\|>-\\|//\\)[[:space:]]*[[(]?"
+  "[[:space:]]*\\(THEN1\\|THENL\\|THEN\\|>>\\|>|\\|>-\\|\\\\\\\\\\)[[:space:]]*[[(]?"
   "Regular expression for strings used to put tactics together.")
 
 (defun tactic-cleanup (string)