fix(shell/lean_js): the and_comm name is taken now

2016-12-31 15:19:58 +01:00 · 2016-12-31 15:19:58 +01:00 · ae7c8f4070
commit ae7c8f4070
parent c5e0ea2600
1 changed files with 1 additions and 1 deletions
--- a/src/shell/lean_js.html
+++ b/src/shell/lean_js.html
@ -58,7 +58,7 @@ outputLog('--- Import complete. ' + checkTimer());
 outputLog('--- Writing test.lean to virtual FS...'); startTimer();
 testfile = ''
         + 'variables p q r s : Prop\n'
-         + 'theorem and_comm : p ∧ q ↔ q ∧ p :=\n'
+         + 'theorem my_and_comm : p ∧ q ↔ q ∧ p :=\n'
         + 'iff.intro\n'
         + '  (assume Hpq : p ∧ q,\n'
         + '    and.intro (and.elim_right Hpq) (and.elim_left Hpq))\n'