Remove usages of MathJax in examples

The MathJax CDN on `http://cdn.mathjax.org` was retired in 2017.

examples/literate_beluga/0Beginner/Close_Terms.bel

@@ -7,7 +7,7 @@
 %{{
 # Closing terms with free variables
 
-We'll first defining what terms are in the untyped lambda calculus.
+We'll first be defining what terms are in the untyped lambda calculus.
 }}%
 
 LF tm : type =

examples/literate_beluga/0Beginner/Norm.bel

@@ -1,8 +1,8 @@
 % Author: Brigitte Pientka
+
 %{{
-# Normalizing lambda-terms
-}}%
-%{{
+# Normalizing lambda-Terms
+
 ## Syntax
 We define first intrinsically well-typed lambda-terms using the base type `nat` and function type.
 }}%

examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Relation.bel

@@ -1,5 +1,6 @@
 %{{
-$Algorithmic Equality for the Untyped Lambda-calculus (R-version)
+# Algorithmic Equality for the Untyped Lambda-calculus (R-version)
+
 We discuss completeness of algorithmic equality for untyped lambda-terms with respect to declarative equality of lambda-terms.
 This case-study is part of [ORBI](https://github.com/pientka/ORBI), Open challenge problem Repository for systems reasoning with Binders.
 For a detailed description of the proof and a discussion regarding other systems see <a href="orbi-jar.pdf" target="_blank">(Felty et al, 2014)</a>.

examples/literate_beluga/0Beginner/Untyped_Algorithmic_Equality_-_Context_Subsumption.bel

@@ -3,6 +3,7 @@
 %
 %{{
 # Algorithmic Equality for the Untyped Lambda-calculus (Generalized context version)
+
 We discuss completeness of algorithmic equality for untyped lambda-terms with respect to declarative equality of lambda-terms.
 This case-study is part of <a ref="https://github.com/pientka/ORBI">ORBI</a>, Open challenge problem Repository for systems reasoning with Binders.
 For a detailed description of the proof and a discussion regarding other systems see <a href="orbi-jar.pdf" target="_blank">(Felty et al, 2014)</a>.

examples/literate_beluga/1Intermediate/Poplmark.bel

@@ -1,11 +1,4 @@
 %{{
-<script type="text/x-mathjax-config">
-  MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}});
-</script>
-<script type="text/javascript"
-  src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
-</script>
-
 # Transitivity of Algorithmic Subtyping
 
 This example follows the proof in the proof pearl description which appeared at TPHOLs2007
@@ -33,7 +26,7 @@ for type variables, but instead we provide for each type variable
 its own reflexivity and transitivity version. In other words, our rule for polymorphic types implements the following:
 $$\frac{\Gamma \vdash T_1 <: S_1 \qquad \Gamma, tr:a <: U \rightarrow U <: T \rightarrow a <: T, w:a <: T, ref : a <: a \vdash S_2 <: T_2 }{\Gamma \vdash \forall a:S_1.S_2(a) <: \forall a:T_1.T_2(a)}$$
 
-We use ($<:$) or `sub` to denote algorithmic subtyping.
+We use (\\(<:\\)) or `sub` to denote algorithmic subtyping.
 }}%
 
 LF sub : tp -> tp -> type =
@@ -59,7 +52,7 @@ schema s_ctx  = some [u:tp] block a:tp, tr:{U:tp}{T:tp} sub a U -> sub U T -> su
 %{{
 ### Reflexivity
 
-**Theorem** :  For every $\Gamma$ and $T$,  $\Gamma\vdash T <: T$.
+**Theorem** :  For every \\(\Gamma\\) and \\(T\\),  \\(\Gamma\vdash T <: T\\).
 
 The reflexivity Theorem is simply described as `{g:s_ctx} {T: [g |- tp]} [g |- sub T T]` in computational-level in Beluga.
 Context variable `g` and term `T` are written explicitly using curly brackets `{g:s_ctx}` and `{T: [g |- tp]}`.
@@ -85,7 +78,7 @@ rec refl : {g:s_ctx} {T: [g |- tp]} [g |- sub T T] =
 %{{
 ### Transitivity
 
-**Theorem** : For every $\Gamma$, $S$, $Q$ and $T$, if $\Gamma\vdash S <: Q$ and $\Gamma\vdash Q <: T$, then $\Gamma\vdash S <: T$.
+**Theorem** : For every \\(\Gamma\\), \\(S\\), \\(Q\\) and \\(T\\), if \\(\Gamma\vdash S <: Q\\) and \\(\Gamma\vdash Q <: T\\), then \\(\Gamma\vdash S <: T\\).
 
 The transitivity Theorem is described  as `(g:s_ctx){Q:[g |- tp]}[g |- sub S Q] -> [g |- sub Q T] -> [g |- sub S T]`.
 The context variable is written implicitly in round bracket as `(g:s_ctx)`.
@@ -168,7 +161,7 @@ Recall `D2` is a parametric and hypothetical derivation which can be viewed as a
 ## Declarative subtyping
 
 We can also define declarative subtyping in Beluga and prove the equivalence between algoritmic and declarative subtyping through soundness and completeness proofs.
-We use ($<$) or `subtype` to denote declarative subtyping.
+We use (\\(<\\)) or `subtype` to denote declarative subtyping.
 }}%
 
 
@@ -195,7 +188,7 @@ schema ss_ctx = some [u:tp] block a:tp, tr:{U:tp}{T:tp} sub a U -> sub U T -> su
 %{{
 ### Soundness
 
-**Theorem** :  For every $\Gamma$, $T$ and $S$, if $\Gamma\vdash T<:S$, then $\Gamma\vdash T < S$ .
+**Theorem** : For every \\(\Gamma\\), \\(T\\) and \\(S\\), if \\(\Gamma\vdash T<:S\\), then \\(\Gamma\vdash T < S\\) .
 }}%
 
 rec sound : (g:ss_ctx) [g |- sub T S] -> [g |- subtype T S] =
@@ -230,7 +223,7 @@ rec sound : (g:ss_ctx) [g |- sub T S] -> [g |- subtype T S] =
 %{{
 ### Completeness
 
-**Theorem**: For every $\Gamma$, $T$ and $S$, if $\Gamma\vdash T < S$, then $\Gamma\vdash T <: S$.
+**Theorem**: For every \\(\Gamma\\), \\(T\\) and \\(S\\), if \\(\Gamma\vdash T < S\\), then \\(\Gamma\vdash T <: S\\).
 }}%
 
 rec complete : (g:ss_ctx) [g |- subtype T S] -> [g |- sub T S] =

examples/literate_beluga/2Advanced/Normalization_by_Evaluation.bel

@@ -1,15 +1,8 @@
 %{{
-<script type="text/x-mathjax-config">
-  MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}});
-</script>
-<script type="text/javascript"
-  src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
-</script>
-
 # Normalization by Evaluation
 
 This case study shows how to implement a type-preserving normalizer using normalization by evaluation [Berger and Schwichtenberg 1991].
-Here we compute $\eta$-long normal forms for the simply-typed lambda calculus.
+Here we compute \\(\eta\\)-long normal forms for the simply-typed lambda calculus.
 See also [Cave and Pientka 2012] for more information on this example.
 
 The setup is a standard intrinsically-typed lambda calculus:
@@ -26,7 +19,7 @@ lam : (tm T -> tm S) -> tm (arr T S).
 schema tctx = tm T;
 
 %{{
-Below, we describe $\eta$-long normal forms. Notice that we allow embedding of neutral terms into normal terms only at base type `b`: this enforces $\eta$-longness.
+Below, we describe \\(\eta\\)-long normal forms. Notice that we allow embedding of neutral terms into normal terms only at base type `b`: this enforces \\(\eta\\)-longness.
 }}%
 
 neut : tp -> type.       --name neut R.

examples/literate_beluga/2Advanced/Weak_Normalization.bel

@@ -125,7 +125,7 @@ mlam MS => fn r => case r of
 %{{
 The trivial fact that reducible terms halt has a corresponding
 trivial proof, analyzing the construction of the the proof of
-'Reduce[|- T] [|- M]'
+`Reduce [|- T] [|- M]`
 }}%
 
 rec reduce_halts : Reduce [|- T] [ |- M] -> [ |- halts M] =