--- a/NEWS Wed Feb 24 18:39:24 2010 +0100
+++ b/NEWS Wed Feb 24 22:45:14 2010 +0100
@@ -38,6 +38,8 @@
and ML_command "set Syntax.trace_ast" help to diagnose syntax
problems.
+* Type constructors admit general mixfix syntax, not just infix.
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 22:45:14 2010 +0100
@@ -13,14 +13,14 @@
\end{matharray}
\begin{rail}
- 'typedecl' typespec infix?
+ 'typedecl' typespec mixfix?
;
'typedef' altname? abstype '=' repset
;
altname: '(' (name | 'open' | 'open' name) ')'
;
- abstype: typespec infix?
+ abstype: typespec mixfix?
;
repset: term ('morphisms' name name)?
;
@@ -367,7 +367,7 @@
'rep\_datatype' ('(' (name +) ')')? (term +)
;
- dtspec: parname? typespec infix? '=' (cons + '|')
+ dtspec: parname? typespec mixfix? '=' (cons + '|')
;
cons: name ( type * ) mixfix?
\end{rail}
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 24 22:45:14 2010 +0100
@@ -244,11 +244,9 @@
section {* Mixfix annotations *}
text {* Mixfix annotations specify concrete \emph{inner syntax} of
- Isabelle types and terms. Some commands such as @{command
- "typedecl"} admit infixes only, while @{command "definition"} etc.\
- support the full range of general mixfixes and binders. Fixed
- parameters in toplevel theorem statements, locale specifications
- also admit mixfix annotations.
+ Isabelle types and terms. Locally fixed parameters in toplevel
+ theorem statements, locale specifications etc.\ also admit mixfix
+ annotations.
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
\begin{rail}
--- a/doc-src/IsarRef/Thy/Spec.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Wed Feb 24 22:45:14 2010 +0100
@@ -959,9 +959,9 @@
\end{matharray}
\begin{rail}
- 'types' (typespec '=' type infix? +)
+ 'types' (typespec '=' type mixfix? +)
;
- 'typedecl' typespec infix?
+ 'typedecl' typespec mixfix?
;
'arities' (nameref '::' arity +)
;
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 24 18:39:24 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 24 22:45:14 2010 +0100
@@ -33,14 +33,14 @@
\end{matharray}
\begin{rail}
- 'typedecl' typespec infix?
+ 'typedecl' typespec mixfix?
;
'typedef' altname? abstype '=' repset
;
altname: '(' (name | 'open' | 'open' name) ')'
;
- abstype: typespec infix?
+ abstype: typespec mixfix?
;
repset: term ('morphisms' name name)?
;
@@ -372,7 +372,7 @@
'rep\_datatype' ('(' (name +) ')')? (term +)
;
- dtspec: parname? typespec infix? '=' (cons + '|')
+ dtspec: parname? typespec mixfix? '=' (cons + '|')
;
cons: name ( type * ) mixfix?
\end{rail}
@@ -906,6 +906,9 @@
\item[iterations] sets how many sets of assignments are
generated for each particular size.
+ \item[no\_assms] specifies whether assumptions in
+ structured proofs should be ignored.
+
\end{description}
These option can be given within square brackets.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 24 18:39:24 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 24 22:45:14 2010 +0100
@@ -266,10 +266,9 @@
%
\begin{isamarkuptext}%
Mixfix annotations specify concrete \emph{inner syntax} of
- Isabelle types and terms. Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\
- support the full range of general mixfixes and binders. Fixed
- parameters in toplevel theorem statements, locale specifications
- also admit mixfix annotations.
+ Isabelle types and terms. Locally fixed parameters in toplevel
+ theorem statements, locale specifications etc.\ also admit mixfix
+ annotations.
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
\begin{rail}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Feb 24 18:39:24 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Feb 24 22:45:14 2010 +0100
@@ -996,9 +996,9 @@
\end{matharray}
\begin{rail}
- 'types' (typespec '=' type infix? +)
+ 'types' (typespec '=' type mixfix? +)
;
- 'typedecl' typespec infix?
+ 'typedecl' typespec mixfix?
;
'arities' (nameref '::' arity +)
;
--- a/src/HOL/Algebra/Congruence.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy Wed Feb 24 22:45:14 2010 +0100
@@ -35,15 +35,17 @@
eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
"is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
-syntax
+abbreviation
not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
- not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
- set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+ where "x .\<noteq>\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)"
-translations
- "x .\<noteq>\<index> y" == "~(x .=\<index> y)"
- "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
- "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
+abbreviation
+ not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
+ where "x .\<notin>\<^bsub>S\<^esub> A == ~(x .\<in>\<^bsub>S\<^esub> A)"
+
+abbreviation
+ set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+ where "A {.\<noteq>}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)"
locale equivalence =
fixes S (structure)
--- a/src/HOL/Bali/Basis.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Feb 24 22:45:14 2010 +0100
@@ -222,12 +222,12 @@
section "quantifiers for option type"
syntax
- Oall :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10)
- Oex :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10)
+ "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10)
+ "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10)
syntax (symbols)
- Oall :: "[pttrn, 'a option, bool] => bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
- Oex :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
+ "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
+ "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
translations
"! x:A: P" == "! x:CONST Option.set A. P"
--- a/src/HOL/Bali/Table.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Bali/Table.thy Wed Feb 24 22:45:14 2010 +0100
@@ -37,11 +37,9 @@
section "map of / table of"
-syntax
- table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
-
abbreviation
- "table_of \<equiv> map_of"
+ table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
+ where "table_of \<equiv> map_of"
translations
(type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Feb 24 22:45:14 2010 +0100
@@ -256,8 +256,8 @@
(* Special syntax for guarded statements and guarded array updates: *)
syntax
- guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
- array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
+ "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
+ "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
translations
"P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
"a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
--- a/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:45:14 2010 +0100
@@ -60,9 +60,8 @@
("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
"|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
-syntax (xsymbols)
- Valid :: "'a bexp => 'a com => 'a bexp => bool"
- ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+notation (xsymbols)
+ Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
lemma ValidI [intro?]:
"(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
--- a/src/HOL/Library/Multiset.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Feb 24 22:45:14 2010 +0100
@@ -1502,13 +1502,13 @@
by (cases M) auto
syntax
- comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+ "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
("({#_/. _ :# _#})")
translations
"{#e. x:#M#}" == "CONST image_mset (%x. e) M"
syntax
- comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
("({#_/ | _ :# _./ _#})")
translations
"{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 22:45:14 2010 +0100
@@ -66,9 +66,8 @@
| Some x \<Rightarrow> frs = []"
-syntax (xsymbols)
- correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
- ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
+notation (xsymbols)
+ correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
lemma sup_ty_opt_OK:
--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 22:45:14 2010 +0100
@@ -59,15 +59,11 @@
"sup_state_opt G == Opt.le (sup_state G)"
-syntax (xsymbols)
- sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=o _" [71,71] 70)
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=l _" [71,71] 70)
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=s _" [71,71] 70)
- sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70)
+notation (xsymbols)
+ sup_ty_opt ("_ \<turnstile> _ <=o _" [71,71] 70) and
+ sup_loc ("_ \<turnstile> _ <=l _" [71,71] 70) and
+ sup_state ("_ \<turnstile> _ <=s _" [71,71] 70) and
+ sup_state_opt ("_ \<turnstile> _ <=' _" [71,71] 70)
lemma JVM_states_unfold:
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:45:14 2010 +0100
@@ -19,9 +19,8 @@
comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
"comb_nil a == ([], a)"
-syntax (xsymbols)
- "comb" :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
- (infixr "\<box>" 55)
+notation (xsymbols)
+ comb (infixr "\<box>" 55)
lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
by (simp add: comb_def comb_nil_def split_beta)
--- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 22:45:14 2010 +0100
@@ -32,16 +32,19 @@
"lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(*<*)
-syntax
- (* allow \<sub> instead of \<bsub>..\<esub> *)
- "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
- "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
- "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+(* allow \<sub> instead of \<bsub>..\<esub> *)
+
+abbreviation (input)
+ lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
+ where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
-translations
- "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
- "x \<sqsubset>\<^sub>r y" => "x \<sqsubset>\<^bsub>r\<^esub> y"
- "x \<squnion>\<^sub>f y" => "x \<squnion>\<^bsub>f\<^esub> y"
+abbreviation (input)
+ lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
+ where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y"
+
+abbreviation (input)
+ plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+ where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
(*>*)
defs
--- a/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 22:45:14 2010 +0100
@@ -38,24 +38,13 @@
xconf (heap (store s)) (abrupt s)"
-syntax (xsymbols)
- hext :: "aheap => aheap => bool"
- ("_ \<le>| _" [51,51] 50)
-
- conf :: "'c prog => aheap => val => ty => bool"
- ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
-
- lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
- ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
-
- oconf :: "'c prog => aheap => obj => bool"
- ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
-
- hconf :: "'c prog => aheap => bool"
- ("_ \<turnstile>h _ \<surd>" [51,51] 50)
-
- conforms :: "state => java_mb env' => bool"
- ("_ ::\<preceq> _" [51,51] 50)
+notation (xsymbols)
+ hext ("_ \<le>| _" [51,51] 50) and
+ conf ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
+ lconf ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
+ oconf ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
+ hconf ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
+ conforms ("_ ::\<preceq> _" [51,51] 50)
section "hext"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 22:45:14 2010 +0100
@@ -123,19 +123,15 @@
| Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
-consts
- "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
+constdefs
+ exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
("_ |- _ -jvmd-> _" [61,61,61]60)
+ "G |- s -jvmd-> t \<equiv>
+ (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
+ {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
-syntax (xsymbols)
- "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
- ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
-
-defs
- exec_all_d_def:
- "G \<turnstile> s -jvmd\<rightarrow> t \<equiv>
- (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
- {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
+notation (xsymbols)
+ exec_all_d ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
declare split_paired_All [simp del]
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 22:45:14 2010 +0100
@@ -32,9 +32,8 @@
"G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-syntax (xsymbols)
- exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
+notation (xsymbols)
+ exec_all ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
text {*
The start configuration of the JVM: in the start heap, we call a
--- a/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 22:45:14 2010 +0100
@@ -33,14 +33,14 @@
cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60)
"A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
-syntax (xsymbols)
- valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60)
- envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60)
- nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60)
- cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
-cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
+notation (xsymbols)
+ valid ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
+ evalid ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
+ nvalid ("\<Turnstile>_: _" [61,61] 60) and
+ envalid ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and
+ nvalids ("|\<Turnstile>_: _" [61,61] 60) and
+ cnvalids ("_ |\<Turnstile>/ _" [61,61] 60) and
+ cenvalid ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
@@ -164,10 +164,10 @@
"MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n\<rightarrow> t)"
MGTe :: "expr => state => etriple"
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
-syntax (xsymbols)
- MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
-syntax (HTML output)
- MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
+notation (xsymbols)
+ MGTe ("MGT\<^sub>e")
+notation (HTML output)
+ MGTe ("MGT\<^sub>e")
lemma MGF_implies_complete:
"\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
--- a/src/HOL/NanoJava/State.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Feb 24 22:45:14 2010 +0100
@@ -84,9 +84,9 @@
lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)"
-syntax (xsymbols)
- hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000)
- lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
+notation (xsymbols)
+ hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and
+ lupd ("lupd'(_\<mapsto>_')" [10,10] 1000)
constdefs
--- a/src/HOL/Nominal/Nominal.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Nominal/Nominal.thy Wed Feb 24 22:45:14 2010 +0100
@@ -3403,13 +3403,13 @@
where
ABS_in: "(abs_fun a x)\<in>ABS_set"
-typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
+typedef (ABS) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+ "ABS_set::('x\<Rightarrow>('a noption)) set"
proof
fix x::"'a" and a::"'x"
show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
qed
-syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
section {* lemmas for deciding permutation equations *}
(*===================================================*)
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Feb 24 22:45:14 2010 +0100
@@ -2079,7 +2079,7 @@
local structure P = OuterParse and K = OuterKeyword in
val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
(P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
fun mk_datatype args =
--- a/src/HOL/TLA/Action.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/TLA/Action.thy Wed Feb 24 22:45:14 2010 +0100
@@ -33,7 +33,7 @@
syntax
(* Syntax for writing action expressions in arbitrary contexts *)
- "ACT" :: "lift => 'a" ("(ACT _)")
+ "_ACT" :: "lift => 'a" ("(ACT _)")
"_before" :: "lift => lift" ("($_)" [100] 99)
"_after" :: "lift => lift" ("(_$)" [100] 99)
--- a/src/HOL/TLA/Intensional.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/TLA/Intensional.thy Wed Feb 24 22:45:14 2010 +0100
@@ -51,7 +51,7 @@
"_holdsAt" :: "['a, lift] => bool" ("(_ |= _)" [100,10] 10)
(* Syntax for lifted expressions outside the scope of |- or |= *)
- "LIFT" :: "lift => 'a" ("LIFT _")
+ "_LIFT" :: "lift => 'a" ("LIFT _")
(* generic syntax for lifted constants and functions *)
"_const" :: "'a => lift" ("(#_)" [1000] 999)
--- a/src/HOL/TLA/Stfun.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/TLA/Stfun.thy Wed Feb 24 22:45:14 2010 +0100
@@ -35,7 +35,7 @@
stvars :: "'a stfun => bool"
syntax
- "PRED" :: "lift => 'a" ("PRED _")
+ "_PRED" :: "lift => 'a" ("PRED _")
"_stvars" :: "lift => bool" ("basevars _")
translations
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Feb 24 22:45:14 2010 +0100
@@ -731,7 +731,7 @@
in (names, specs) end;
val parse_datatype_decl =
- (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+ (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
(P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Wed Feb 24 22:45:14 2010 +0100
@@ -296,7 +296,7 @@
val quotspec_parser =
OuterParse.and_list1
((OuterParse.type_args -- OuterParse.binding) --
- OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
+ OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
(OuterParse.$$$ "/" |-- OuterParse.term))
val _ = OuterKeyword.keyword "/"
--- a/src/HOL/Tools/typedef.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Wed Feb 24 22:45:14 2010 +0100
@@ -255,7 +255,7 @@
(Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.binding ||
P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
>> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
Toplevel.print o Toplevel.theory_to_proof
--- a/src/HOL/UNITY/SubstAx.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Wed Feb 24 22:45:14 2010 +0100
@@ -17,8 +17,8 @@
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60)
"A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
-syntax (xsymbols)
- "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
+notation (xsymbols)
+ LeadsTo (infixl " \<longmapsto>w " 60)
text{*Resembles the previous definition of LeadsTo*}
--- a/src/HOL/UNITY/WFair.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOL/UNITY/WFair.thy Wed Feb 24 22:45:14 2010 +0100
@@ -69,8 +69,8 @@
--{*predicate transformer: the largest set that leads to @{term B}*}
"wlt F B == Union {A. F \<in> A leadsTo B}"
-syntax (xsymbols)
- "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
+notation (xsymbols)
+ leadsTo (infixl "\<longmapsto>" 60)
subsection{*transient*}
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 22:45:14 2010 +0100
@@ -24,25 +24,25 @@
IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 25)
-syntax ("" output)
- "NOT" ::"'a predicate => 'a predicate" ("~ _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "&" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "|" 30)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25)
+notation (output)
+ NOT ("~ _" [40] 40) and
+ AND (infixr "&" 35) and
+ OR (infixr "|" 30) and
+ IMPLIES (infixr "-->" 25)
-syntax (xsymbols output)
- "NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<longrightarrow>" 25)
+notation (xsymbols output)
+ NOT ("\<not> _" [40] 40) and
+ AND (infixr "\<and>" 35) and
+ OR (infixr "\<or>" 30) and
+ IMPLIES (infixr "\<longrightarrow>" 25)
-syntax (xsymbols)
- "satisfies" ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
+notation (xsymbols)
+ satisfies ("_ \<Turnstile> _" [100,9] 8)
-syntax (HTML output)
- "NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
+notation (HTML output)
+ NOT ("\<not> _" [40] 40) and
+ AND (infixr "\<and>" 35) and
+ OR (infixr "\<or>" 30)
defs
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Feb 24 22:45:14 2010 +0100
@@ -291,7 +291,7 @@
|| Scan.succeed [];
val domain_decl =
- (type_args' -- P.binding -- P.opt_infix) --
+ (type_args' -- P.binding -- P.opt_mixfix) --
(P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Feb 24 22:45:14 2010 +0100
@@ -700,7 +700,7 @@
val parse_domain_iso :
(string list * binding * mixfix * string * (binding * binding) option)
parser =
- (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ) --
+ (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
--- a/src/HOLCF/Tools/pcpodef.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Wed Feb 24 22:45:14 2010 +0100
@@ -340,7 +340,7 @@
Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
--| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
--- a/src/HOLCF/Tools/repdef.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Wed Feb 24 22:45:14 2010 +0100
@@ -167,7 +167,7 @@
Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
--| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
--- a/src/Pure/Isar/isar_syn.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Feb 24 22:45:14 2010 +0100
@@ -104,13 +104,13 @@
val _ =
OuterSyntax.command "typedecl" "type declaration" K.thy_decl
- (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) =>
+ (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
- (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
+ (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
>> (Toplevel.theory o Sign.add_tyabbrs o
map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
--- a/src/Pure/Isar/outer_parse.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/Pure/Isar/outer_parse.ML Wed Feb 24 22:45:14 2010 +0100
@@ -72,8 +72,6 @@
val typ: string parser
val mixfix: mixfix parser
val mixfix': mixfix parser
- val opt_infix: mixfix parser
- val opt_infix': mixfix parser
val opt_mixfix: mixfix parser
val opt_mixfix': mixfix parser
val where_: string parser
@@ -279,8 +277,6 @@
val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
-val opt_infix = opt_annotation !!! (infxl || infxr || infx);
-val opt_infix' = opt_annotation I (infxl || infxr || infx);
val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
--- a/src/Pure/Syntax/mixfix.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Feb 24 22:45:14 2010 +0100
@@ -101,20 +101,26 @@
fun syn_ext_types type_decls =
let
- fun mk_infix sy t p1 p2 p3 =
- SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
- [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3);
+ fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
+ fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
fun mfix_of (_, _, NoSyn) = NONE
- | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p)
- | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p)
- | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p)
- | mfix_of (t, _, _) =
- error ("Bad mixfix declaration for type: " ^ quote t); (* FIXME printable!? *)
+ | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
+ | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
+ | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
+ | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
+ | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
+ | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *)
- val mfix = map_filter mfix_of type_decls;
+ fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
+ if SynExt.mfix_args sy = n then ()
+ else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
+ | check_args _ NONE = ();
+
+ val mfix = map mfix_of type_decls;
+ val _ = map2 check_args type_decls mfix;
val xconsts = map #1 type_decls;
- in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
+ in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
(* syn_ext_consts *)
@@ -140,7 +146,7 @@
| mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
| mfix_of (c, ty, Binder (sy, p, q)) =
[SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
- | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c);
+ | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *)
fun binder (c, _, Binder _) = SOME (binder_name c, c)
| binder _ = NONE;
--- a/src/Pure/Syntax/syn_ext.ML Wed Feb 24 18:39:24 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Wed Feb 24 22:45:14 2010 +0100
@@ -28,6 +28,8 @@
val cargs: string
val any: string
val sprop: string
+ datatype mfix = Mfix of string * typ * string * int list * int
+ val err_in_mfix: string -> mfix -> 'a
val typ_to_nonterm: typ -> string
datatype xsymb =
Delim of string |
@@ -37,7 +39,6 @@
datatype xprod = XProd of string * xsymb list * string * int
val chain_pri: int
val delims_of: xprod list -> string list list
- datatype mfix = Mfix of string * typ * string * int list * int
datatype syn_ext =
SynExt of {
xprods: xprod list,
--- a/src/Sequents/LK0.thy Wed Feb 24 18:39:24 2010 +0100
+++ b/src/Sequents/LK0.thy Wed Feb 24 22:45:14 2010 +0100
@@ -43,23 +43,23 @@
not_equal (infixl "~=" 50) where
"x ~= y == ~ (x = y)"
-syntax (xsymbols)
- Not :: "o => o" ("\<not> _" [40] 40)
- conj :: "[o, o] => o" (infixr "\<and>" 35)
- disj :: "[o, o] => o" (infixr "\<or>" 30)
- imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
- iff :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
- All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+notation (xsymbols)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ not_equal (infixl "\<noteq>" 50)
-syntax (HTML output)
- Not :: "o => o" ("\<not> _" [40] 40)
- conj :: "[o, o] => o" (infixr "\<and>" 35)
- disj :: "[o, o] => o" (infixr "\<or>" 30)
- All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+notation (HTML output)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ not_equal (infixl "\<noteq>" 50)
local