# HG changeset patch
# User wenzelm
# Date 1295901033 -3600
# Node ID ed4d793f0c26a689866f73f8a251f16dd4829fa0
# Parent 0040e0ea02e7ea276890399fba77e71f741fb356
improved README -- Isabelle symbols and fonts;
diff -r 0040e0ea02e7 -r ed4d793f0c26 src/Tools/jEdit/dist-template/README.html
--- a/src/Tools/jEdit/dist-template/README.html Mon Jan 24 15:39:42 2011 +0100
+++ b/src/Tools/jEdit/dist-template/README.html Mon Jan 24 21:30:33 2011 +0100
@@ -1,4 +1,4 @@
-
+
@@ -9,7 +9,7 @@
-Notes on the Isabelle/jEdit Prover IDE
+The Isabelle/jEdit Prover IDE
+
+Isabelle symbols and fonts
+
+
+
+ - Isabelle supports infinitely many symbols:
+ α, β, γ, …
+ ∀, ∃, ∨, ∧, ⟶, ⟷, …
+ ≤, ≥, ⊓, ⊔, …
+ ℵ, △, ∇, …
+ \<foo>, \<bar>, \<baz>, …
+
+
+ - A default mapping relates some Isabelle symbols to Unicode points
+ (see $ISABELLE_HOME/etc/symbols and $ISABELLE_HOME_USER/etc/symbols).
+
+
+ - The IsabelleText font ensures that Unicode points are actually
+ seen on the screen (or printer).
+
+
+ - Input methods:
+
+ - copy/paste from decoded source files
+ - copy/paste from prover output
+ - completion provided by Isabelle plugin, e.g.
+
+
+ | name | abbreviation | symbol |
|---|
+
+ | lambda | | λ |
+ | Rightarrow | => | ⇒ |
+ | Longrightarrow | ==> | ⟹ |
+
+ | And | !! | ⋀ |
+ | equiv | == | ≡ |
+
+ | forall | ! | ∀ |
+ | exists | ? | ∃ |
+ | longrightarrow | --> | ⟶ |
+ | and | /\ | ∧ |
+ | or | \/ | ∨ |
+ | not | ~ | ¬ |
+ | noteq | ~= | ≠ |
+ | in | : | ∈ |
+ | notin | ~: | ∉ |
+
+
+
+
+
+ - NOTE: The above abbreviations refer to the input method.
+ The logical notation provides ASCII alternatives that often
+ coincide, but deviate occasionally.
+
+
+ - NOTE: Generic jEdit abbreviations or plugins perform similar
+ source replacement operations; this works for Isabelle as long
+ as the Unicode sequences coincide with the symbol mapping.
+
+
+
+
+
Limitations and workrounds (January 2011)