--- a/doc-src/IsarRef/Thy/Quick_Reference.thy Mon Nov 15 17:52:48 2010 +0100
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy Mon Nov 15 18:04:04 2010 +0100
@@ -22,14 +22,14 @@
@{command "next"} & switch blocks \\
@{command "note"}~@{text "a = b"} & reconsider facts \\
@{command "let"}~@{text "p = t"} & abbreviate terms by higher-order matching \\
+ @{command "write"}~@{text "c (mx)"} & declare local mixfix syntax \\
\end{tabular}
\medskip
\begin{tabular}{rcl}
- @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof |"}~~@{command "definition"}~@{text "\<dots> | \<dots>"} \\[1ex]
@{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\
- & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
+ & @{text "|"} & @{text "prfx\<^sup>*"}~@{command "done"} \\[0.5ex]
@{text prfx} & = & @{command "apply"}~@{text method} \\
& @{text "|"} & @{command "using"}~@{text "facts"} \\
& @{text "|"} & @{command "unfolding"}~@{text "facts"} \\
@@ -37,6 +37,7 @@
& @{text "|"} & @{command "next"} \\
& @{text "|"} & @{command "note"}~@{text "name = facts"} \\
& @{text "|"} & @{command "let"}~@{text "term = term"} \\
+ & @{text "|"} & @{command "write"}~@{text "name (mixfix)"} \\
& @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\
& @{text "|"} & @{command "assume"}~@{text "name: props"} \\
& @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
@@ -57,7 +58,7 @@
@{command "hence"} & @{text "\<equiv>"} & @{command "then"}~@{command "have"} \\
@{command "thus"} & @{text "\<equiv>"} & @{command "then"}~@{command "show"} \\
@{command "from"}~@{text a} & @{text "\<equiv>"} & @{command "note"}~@{text a}~@{command "then"} \\
- @{command "with"}~@{text a} & @{text "\<equiv>"} & @{command "from"}~@{text "a \<AND> this"} \\[1ex]
+ @{command "with"}~@{text a} & @{text "\<equiv>"} & @{command "from"}~@{text "a \<AND> this"} \\[0.5ex]
@{command "from"}~@{text this} & @{text "\<equiv>"} & @{command "then"} \\
@{command "from"}~@{text this}~@{command "have"} & @{text "\<equiv>"} & @{command "hence"} \\
@{command "from"}~@{text this}~@{command "show"} & @{text "\<equiv>"} & @{command "thus"} \\
@@ -99,9 +100,9 @@
\begin{tabular}{ll}
@{command "pr"} & print current state \\
@{command "thm"}~@{text a} & print fact \\
+ @{command "prop"}~@{text \<phi>} & print proposition \\
@{command "term"}~@{text t} & print term \\
- @{command "prop"}~@{text \<phi>} & print meta-level proposition \\
- @{command "typ"}~@{text \<tau>} & print meta-level type \\
+ @{command "typ"}~@{text \<tau>} & print type \\
\end{tabular}
*}
--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex Mon Nov 15 17:52:48 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex Mon Nov 15 18:04:04 2010 +0100
@@ -44,14 +44,14 @@
\hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} & switch blocks \\
\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequote}}} & reconsider facts \\
\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} & abbreviate terms by higher-order matching \\
+ \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ \ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & declare local mixfix syntax \\
\end{tabular}
\medskip
\begin{tabular}{rcl}
- \isa{{\isaliteral{22}{\isachardoublequote}}theory{\isaliteral{5C3C646173683E}{\isasymdash}}stmt{\isaliteral{22}{\isachardoublequote}}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ props\ proof\ \ {\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
\isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{22}{\isachardoublequote}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}\ stmt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}} \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\[1ex]
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prfx\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\[0.5ex]
\isa{prfx} & = & \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}facts{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}facts{\isaliteral{22}{\isachardoublequote}}} \\
@@ -59,6 +59,7 @@
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ facts{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}term\ {\isaliteral{3D}{\isacharequal}}\ term{\isaliteral{22}{\isachardoublequote}}} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{28}{\isacharparenleft}}mixfix{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}var\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ props{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}~\isa{goal} \\
@@ -81,7 +82,7 @@
\hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} \\
\hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{a}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\
- \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}} \\[1ex]
+ \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ this{\isaliteral{22}{\isachardoublequote}}} \\[0.5ex]
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.hence}{\mbox{\isa{\isacommand{hence}}}} \\
\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{this}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} & \hyperlink{command.thus}{\mbox{\isa{\isacommand{thus}}}} \\
@@ -127,9 +128,9 @@
\begin{tabular}{ll}
\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}} & print current state \\
\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{a} & print fact \\
+ \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} & print proposition \\
\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} & print term \\
- \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} & print meta-level proposition \\
- \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} & print meta-level type \\
+ \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} & print type \\
\end{tabular}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Nov 15 17:52:48 2010 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Nov 15 18:04:04 2010 +0100
@@ -244,6 +244,10 @@
done
qed
+section {* Setup for String.literal *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
+
section {* Simplification rules for optimisation *}
lemma [code_pred_simp]: "\<not> False == True"
--- a/src/HOL/Library/Quotient_Option.thy Mon Nov 15 17:52:48 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Mon Nov 15 18:04:04 2010 +0100
@@ -9,7 +9,7 @@
begin
fun
- option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
+ option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
where
"option_rel R None None = True"
| "option_rel R (Some x) None = False"
--- a/src/HOL/Library/Quotient_Product.thy Mon Nov 15 17:52:48 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Mon Nov 15 18:04:04 2010 +0100
@@ -9,7 +9,7 @@
begin
definition
- prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+ prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
--- a/src/HOL/Library/Quotient_Sum.thy Mon Nov 15 17:52:48 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Mon Nov 15 18:04:04 2010 +0100
@@ -9,7 +9,7 @@
begin
fun
- sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+ sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
where
"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
--- a/src/Tools/jEdit/README Mon Nov 15 17:52:48 2010 +0100
+++ b/src/Tools/jEdit/README Mon Nov 15 18:04:04 2010 +0100
@@ -60,10 +60,12 @@
used in Isabelle sub/superscripts).
-Windows/Linux
-=============
+Known problems with OpenJDK
+===========================
-- Works best with Sun Java 1.6.x -- avoid OpenJDK for now.
+- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
+ the jEdit text area. Always use official JRE 1.6.x from
+ Sun/Oracle/Apple.
Licenses and home sites of contributing systems
@@ -77,7 +79,3 @@
* Lobo/Cobra: GPL and LGPL
http://lobobrowser.org/
-
-
- Makarius
- 31-May-2010