Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
authorwenzelm
Thu Nov 20 00:03:47 2008 +0100 (2008-11-20)
changeset 288565e009a80fe6d
parent 28855 5d21a3e7303c
child 28857 87d638a4ee67
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
NEWS
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/Proof.thy
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/HOL/Code_Setup.thy
src/HOL/Groebner_Basis.thy
src/HOL/HOL.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Dense_Linear_Order.thy
src/Pure/Isar/proof_context.ML
src/Pure/Pure.thy
src/Pure/Syntax/simple_syntax.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/conjunction.ML
src/Pure/logic.ML
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/NEWS	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -47,6 +47,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Slightly more coherent Pure syntax, with updated documentation in
     1.8 +isar-ref manual.  Removed locales meta_term_syntax and
     1.9 +meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
    1.10 +INCOMPATIBILITY in rare situations.
    1.11 +
    1.12  * Goal-directed proof now enforces strict proof irrelevance wrt. sort
    1.13  hypotheses.  Sorts required in the course of reasoning need to be
    1.14  covered by the constraints in the initial statement, completed by the
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Nov 19 18:15:31 2008 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 20 00:03:47 2008 +0100
     2.3 @@ -485,6 +485,7 @@
     2.4      & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     2.5      & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     2.6      & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     2.7 +    & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     2.8      & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
     2.9      & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    2.10      & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    2.11 @@ -493,18 +494,21 @@
    2.12      & @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
    2.13      & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
    2.14      & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
    2.15 +    & @{text "|"} & @{verbatim TERM} @{text logic} \\
    2.16      & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
    2.17  
    2.18 -  @{syntax_def (inner) aprop} & = & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
    2.19 +  @{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
    2.20 +    & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
    2.21 +    & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
    2.22      & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
    2.23  
    2.24    @{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
    2.25      & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
    2.26      & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
    2.27 +    & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
    2.28      & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
    2.29      & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
    2.30      & @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
    2.31 -    & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
    2.32      & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
    2.33  
    2.34    @{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  |  id  |  "}@{verbatim "_"} \\
    2.35 @@ -847,7 +851,7 @@
    2.36    Priority information attached to chain productions is ignored; only
    2.37    the dummy value @{text "-1"} is displayed.
    2.38  
    2.39 -  \item @{text "print_modes"} lists the alternative print modes
    2.40 +  \item @{text "print modes"} lists the alternative print modes
    2.41    provided by this grammar; see \secref{sec:print-modes}.
    2.42  
    2.43    \item @{text "parse_rules"} and @{text "print_rules"} relate to
     3.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Wed Nov 19 18:15:31 2008 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 20 00:03:47 2008 +0100
     3.3 @@ -381,7 +381,7 @@
     3.4  
     3.5    Goals may consist of multiple statements, resulting in a list of
     3.6    facts eventually.  A pending multi-goal is internally represented as
     3.7 -  a meta-level conjunction (printed as @{text "&&"}), which is usually
     3.8 +  a meta-level conjunction (@{text "&&&"}), which is usually
     3.9    split into the corresponding number of sub-goals prior to an initial
    3.10    method application, via @{command_ref "proof"}
    3.11    (\secref{sec:proof-steps}) or @{command_ref "apply"}
     4.1 --- a/src/FOL/FOL.thy	Wed Nov 19 18:15:31 2008 +0100
     4.2 +++ b/src/FOL/FOL.thy	Thu Nov 20 00:03:47 2008 +0100
     4.3 @@ -346,9 +346,7 @@
     4.4  lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
     4.5    unfolding atomize_eq induct_equal_def .
     4.6  
     4.7 -lemma induct_conj_eq:
     4.8 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     4.9 -  shows "(A && B) == Trueprop(induct_conj(A, B))"
    4.10 +lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))"
    4.11    unfolding atomize_conj induct_conj_def .
    4.12  
    4.13  lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
     5.1 --- a/src/FOL/IFOL.thy	Wed Nov 19 18:15:31 2008 +0100
     5.2 +++ b/src/FOL/IFOL.thy	Thu Nov 20 00:03:47 2008 +0100
     5.3 @@ -698,11 +698,9 @@
     5.4    then show "A == B" by (rule iff_reflection)
     5.5  qed
     5.6  
     5.7 -lemma atomize_conj [atomize]:
     5.8 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     5.9 -  shows "(A && B) == Trueprop (A & B)"
    5.10 +lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
    5.11  proof
    5.12 -  assume conj: "A && B"
    5.13 +  assume conj: "A &&& B"
    5.14    show "A & B"
    5.15    proof (rule conjI)
    5.16      from conj show A by (rule conjunctionD1)
    5.17 @@ -710,7 +708,7 @@
    5.18    qed
    5.19  next
    5.20    assume conj: "A & B"
    5.21 -  show "A && B"
    5.22 +  show "A &&& B"
    5.23    proof -
    5.24      from conj show A ..
    5.25      from conj show B ..
     6.1 --- a/src/HOL/Code_Setup.thy	Wed Nov 19 18:15:31 2008 +0100
     6.2 +++ b/src/HOL/Code_Setup.thy	Thu Nov 20 00:03:47 2008 +0100
     6.3 @@ -78,9 +78,8 @@
     6.4    using assms by simp_all
     6.5  
     6.6  lemma If_case_cert:
     6.7 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     6.8    assumes "CASE \<equiv> (\<lambda>b. If b f g)"
     6.9 -  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    6.10 +  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
    6.11    using assms by simp_all
    6.12  
    6.13  setup {*
     7.1 --- a/src/HOL/Groebner_Basis.thy	Wed Nov 19 18:15:31 2008 +0100
     7.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Nov 20 00:03:47 2008 +0100
     7.3 @@ -64,10 +64,8 @@
     7.4  subsubsection {* Declaring the abstract theory *}
     7.5  
     7.6  lemma semiring_ops:
     7.7 -  fixes meta_term :: "'a => prop"  ("TERM _")
     7.8    shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
     7.9 -    and "TERM r0" and "TERM r1"
    7.10 -  by rule+
    7.11 +    and "TERM r0" and "TERM r1" .
    7.12  
    7.13  lemma semiring_rules:
    7.14    "add (mul a m) (mul b m) = mul (add a b) m"
    7.15 @@ -226,9 +224,7 @@
    7.16      and sub_add: "sub x y = add x (neg y)"
    7.17  begin
    7.18  
    7.19 -lemma ring_ops:
    7.20 -  fixes meta_term :: "'a => prop"  ("TERM _")
    7.21 -  shows "TERM (sub x y)" and "TERM (neg x)" .
    7.22 +lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
    7.23  
    7.24  lemmas ring_rules = neg_mul sub_add
    7.25  
     8.1 --- a/src/HOL/HOL.thy	Wed Nov 19 18:15:31 2008 +0100
     8.2 +++ b/src/HOL/HOL.thy	Thu Nov 20 00:03:47 2008 +0100
     8.3 @@ -845,11 +845,9 @@
     8.4    then show "x == y" by (rule eq_reflection)
     8.5  qed
     8.6  
     8.7 -lemma atomize_conj [atomize]:
     8.8 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     8.9 -  shows "(A && B) == Trueprop (A & B)"
    8.10 +lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
    8.11  proof
    8.12 -  assume conj: "A && B"
    8.13 +  assume conj: "A &&& B"
    8.14    show "A & B"
    8.15    proof (rule conjI)
    8.16      from conj show A by (rule conjunctionD1)
    8.17 @@ -857,7 +855,7 @@
    8.18    qed
    8.19  next
    8.20    assume conj: "A & B"
    8.21 -  show "A && B"
    8.22 +  show "A &&& B"
    8.23    proof -
    8.24      from conj show A ..
    8.25      from conj show B ..
    8.26 @@ -1511,9 +1509,7 @@
    8.27  lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
    8.28    by (unfold atomize_eq induct_equal_def)
    8.29  
    8.30 -lemma induct_conj_eq:
    8.31 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    8.32 -  shows "(A && B) == Trueprop (induct_conj A B)"
    8.33 +lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
    8.34    by (unfold atomize_conj induct_conj_def)
    8.35  
    8.36  lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
     9.1 --- a/src/HOL/Library/Coinductive_List.thy	Wed Nov 19 18:15:31 2008 +0100
     9.2 +++ b/src/HOL/Library/Coinductive_List.thy	Thu Nov 20 00:03:47 2008 +0100
     9.3 @@ -216,9 +216,8 @@
     9.4      CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
     9.5  
     9.6  lemma llist_case_cert:
     9.7 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     9.8    assumes "CASE \<equiv> llist_case c d"
     9.9 -  shows "(CASE LNil \<equiv> c) && (CASE (LCons M N) \<equiv> d M N)"
    9.10 +  shows "(CASE LNil \<equiv> c) &&& (CASE (LCons M N) \<equiv> d M N)"
    9.11    using assms by simp_all
    9.12  
    9.13  setup {*
    10.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Wed Nov 19 18:15:31 2008 +0100
    10.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Thu Nov 20 00:03:47 2008 +0100
    10.3 @@ -268,7 +268,6 @@
    10.4  
    10.5  lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
    10.6  lemma atoms:
    10.7 -  fixes meta_term :: "'a => prop"  ("TERM _")
    10.8    shows "TERM (less :: 'a \<Rightarrow> _)"
    10.9      and "TERM (less_eq :: 'a \<Rightarrow> _)"
   10.10      and "TERM (op = :: 'a \<Rightarrow> _)" .
   10.11 @@ -505,7 +504,6 @@
   10.12  lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
   10.13    by (rule constr_dense_linear_order_axioms)
   10.14  lemma atoms:
   10.15 -  fixes meta_term :: "'a => prop"  ("TERM _")
   10.16    shows "TERM (less :: 'a \<Rightarrow> _)"
   10.17      and "TERM (less_eq :: 'a \<Rightarrow> _)"
   10.18      and "TERM (op = :: 'a \<Rightarrow> _)" .
    11.1 --- a/src/Pure/Isar/proof_context.ML	Wed Nov 19 18:15:31 2008 +0100
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 20 00:03:47 2008 +0100
    11.3 @@ -1060,10 +1060,14 @@
    11.4  
    11.5  val _ = Context.>> (Context.map_theory
    11.6   (Sign.add_syntax
    11.7 -   [("_context_const", "id => 'a", Delimfix "CONST _"),
    11.8 -    ("_context_const", "longid => 'a", Delimfix "CONST _"),
    11.9 -    ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
   11.10 -    ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
   11.11 +   [("_context_const", "id => logic", Delimfix "CONST _"),
   11.12 +    ("_context_const", "id => aprop", Delimfix "CONST _"),
   11.13 +    ("_context_const", "longid => logic", Delimfix "CONST _"),
   11.14 +    ("_context_const", "longid => aprop", Delimfix "CONST _"),
   11.15 +    ("_context_xconst", "id => logic", Delimfix "XCONST _"),
   11.16 +    ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
   11.17 +    ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
   11.18 +    ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
   11.19    Sign.add_advanced_trfuns
   11.20      ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
   11.21  
    12.1 --- a/src/Pure/Pure.thy	Wed Nov 19 18:15:31 2008 +0100
    12.2 +++ b/src/Pure/Pure.thy	Thu Nov 20 00:03:47 2008 +0100
    12.3 @@ -24,34 +24,22 @@
    12.4    "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
    12.5  
    12.6  
    12.7 -subsection {* Embedded terms *}
    12.8 -
    12.9 -locale meta_term_syntax =
   12.10 -  fixes meta_term :: "'a => prop"  ("TERM _")
   12.11 -
   12.12 -lemmas [intro?] = termI
   12.13 -
   12.14 -
   12.15  subsection {* Meta-level conjunction *}
   12.16  
   12.17 -locale meta_conjunction_syntax =
   12.18 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   12.19 -
   12.20  lemma all_conjunction:
   12.21 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   12.22 -  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
   12.23 +  "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
   12.24  proof
   12.25 -  assume conj: "!!x. PROP A x && PROP B x"
   12.26 -  show "(!!x. PROP A x) && (!!x. PROP B x)"
   12.27 +  assume conj: "!!x. PROP A x &&& PROP B x"
   12.28 +  show "(!!x. PROP A x) &&& (!!x. PROP B x)"
   12.29    proof -
   12.30      fix x
   12.31      from conj show "PROP A x" by (rule conjunctionD1)
   12.32      from conj show "PROP B x" by (rule conjunctionD2)
   12.33    qed
   12.34  next
   12.35 -  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
   12.36 +  assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
   12.37    fix x
   12.38 -  show "PROP A x && PROP B x"
   12.39 +  show "PROP A x &&& PROP B x"
   12.40    proof -
   12.41      show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
   12.42      show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   12.43 @@ -59,20 +47,19 @@
   12.44  qed
   12.45  
   12.46  lemma imp_conjunction:
   12.47 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   12.48 -  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
   12.49 +  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   12.50  proof
   12.51 -  assume conj: "PROP A ==> PROP B && PROP C"
   12.52 -  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
   12.53 +  assume conj: "PROP A ==> PROP B &&& PROP C"
   12.54 +  show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   12.55    proof -
   12.56      assume "PROP A"
   12.57      from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
   12.58      from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   12.59    qed
   12.60  next
   12.61 -  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
   12.62 +  assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
   12.63    assume "PROP A"
   12.64 -  show "PROP B && PROP C"
   12.65 +  show "PROP B &&& PROP C"
   12.66    proof -
   12.67      from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
   12.68      from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   12.69 @@ -80,18 +67,17 @@
   12.70  qed
   12.71  
   12.72  lemma conjunction_imp:
   12.73 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   12.74 -  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   12.75 +  "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   12.76  proof
   12.77 -  assume r: "PROP A && PROP B ==> PROP C"
   12.78 +  assume r: "PROP A &&& PROP B ==> PROP C"
   12.79    assume ab: "PROP A" "PROP B"
   12.80    show "PROP C"
   12.81    proof (rule r)
   12.82 -    from ab show "PROP A && PROP B" .
   12.83 +    from ab show "PROP A &&& PROP B" .
   12.84    qed
   12.85  next
   12.86    assume r: "PROP A ==> PROP B ==> PROP C"
   12.87 -  assume conj: "PROP A && PROP B"
   12.88 +  assume conj: "PROP A &&& PROP B"
   12.89    show "PROP C"
   12.90    proof (rule r)
   12.91      from conj show "PROP A" by (rule conjunctionD1)
    13.1 --- a/src/Pure/Syntax/simple_syntax.ML	Wed Nov 19 18:15:31 2008 +0100
    13.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Thu Nov 20 00:03:47 2008 +0100
    13.3 @@ -18,7 +18,7 @@
    13.4  (* scanning tokens *)
    13.5  
    13.6  val lexicon = Scan.make_lexicon
    13.7 -  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&", "CONST"]);
    13.8 +  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&&", "CONST"]);
    13.9  
   13.10  fun read scan s =
   13.11    (case
   13.12 @@ -81,7 +81,7 @@
   13.13          | term2
   13.14    term2 = term3 == term2
   13.15          | term3 =?= term2
   13.16 -        | term3 && term2
   13.17 +        | term3 &&& term2
   13.18          | term3
   13.19    term3 = ident :: typ
   13.20          | var :: typ
   13.21 @@ -111,7 +111,7 @@
   13.22    term2 env T) x
   13.23  and term2 env T x =
   13.24   (equal env "==" || equal env "=?=" ||
   13.25 -  term3 env propT -- ($$ "&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   13.26 +  term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   13.27    term3 env T) x
   13.28  and equal env eq x =
   13.29   (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
    14.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Nov 19 18:15:31 2008 +0100
    14.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Nov 20 00:03:47 2008 +0100
    14.3 @@ -10,6 +10,7 @@
    14.4    val dddot_indexname: indexname
    14.5    val constrainC: string
    14.6    val typeT: typ
    14.7 +  val spropT: typ
    14.8    val max_pri: int
    14.9    val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   14.10    val mk_trfun: string * 'a -> string * ('a * stamp)
    15.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 19 18:15:31 2008 +0100
    15.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Nov 20 00:03:47 2008 +0100
    15.3 @@ -473,9 +473,8 @@
    15.4     ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),
    15.5     ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
    15.6    [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
    15.7 -   ("_sort_constraint", sort_constraint_tr), ("\\<^fixed>meta_conjunction", conjunction_tr),
    15.8 -   ("_TYPE", type_tr), ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr),
    15.9 -   ("_index", index_tr)],
   15.10 +   ("_sort_constraint", sort_constraint_tr), ("_TYPE", type_tr),
   15.11 +   ("_DDDOT", dddot_tr), ("_index", index_tr)],
   15.12    ([]: (string * (term list -> term)) list),
   15.13    [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
   15.14     ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
    16.1 --- a/src/Pure/conjunction.ML	Wed Nov 19 18:15:31 2008 +0100
    16.2 +++ b/src/Pure/conjunction.ML	Thu Nov 20 00:03:47 2008 +0100
    16.3 @@ -67,7 +67,7 @@
    16.4  val B = read_prop "B" and vB = read_prop "?B";
    16.5  val C = read_prop "C";
    16.6  val ABC = read_prop "A ==> B ==> C";
    16.7 -val A_B = read_prop "A && B";
    16.8 +val A_B = read_prop "A &&& B";
    16.9  
   16.10  val conjunction_def =
   16.11    Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
   16.12 @@ -135,7 +135,7 @@
   16.13  in
   16.14  
   16.15  (*
   16.16 -   A1 && ... && An ==> B
   16.17 +  A1 &&& ... &&& An ==> B
   16.18    -----------------------
   16.19    A1 ==> ... ==> An ==> B
   16.20  *)
   16.21 @@ -155,7 +155,7 @@
   16.22  (*
   16.23    A1 ==> ... ==> An ==> B
   16.24    -----------------------
   16.25 -  A1 && ... && An ==> B
   16.26 +  A1 &&& ... &&& An ==> B
   16.27  *)
   16.28  fun uncurry_balanced n th =
   16.29    if n < 2 then th
    17.1 --- a/src/Pure/logic.ML	Wed Nov 19 18:15:31 2008 +0100
    17.2 +++ b/src/Pure/logic.ML	Thu Nov 20 00:03:47 2008 +0100
    17.3 @@ -162,33 +162,33 @@
    17.4  val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
    17.5  
    17.6  
    17.7 -(*A && B*)
    17.8 +(*A &&& B*)
    17.9  fun mk_conjunction (A, B) = conjunction $ A $ B;
   17.10  
   17.11 -(*A && B && C -- improper*)
   17.12 +(*A &&& B &&& C -- improper*)
   17.13  fun mk_conjunction_list [] = true_prop
   17.14    | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   17.15  
   17.16 -(*(A && B) && (C && D) -- balanced*)
   17.17 +(*(A &&& B) &&& (C &&& D) -- balanced*)
   17.18  fun mk_conjunction_balanced [] = true_prop
   17.19    | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
   17.20  
   17.21  
   17.22 -(*A && B*)
   17.23 +(*A &&& B*)
   17.24  fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   17.25    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   17.26  
   17.27 -(*A && B && C -- improper*)
   17.28 +(*A &&& B &&& C -- improper*)
   17.29  fun dest_conjunction_list t =
   17.30    (case try dest_conjunction t of
   17.31      NONE => [t]
   17.32    | SOME (A, B) => A :: dest_conjunction_list B);
   17.33  
   17.34 -(*(A && B) && (C && D) -- balanced*)
   17.35 +(*(A &&& B) &&& (C &&& D) -- balanced*)
   17.36  fun dest_conjunction_balanced 0 _ = []
   17.37    | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
   17.38  
   17.39 -(*((A && B) && C) && D && E -- flat*)
   17.40 +(*((A &&& B) &&& C) &&& D &&& E -- flat*)
   17.41  fun dest_conjunctions t =
   17.42    (case try dest_conjunction t of
   17.43      NONE => [t]
    18.1 --- a/src/Pure/pure_thy.ML	Wed Nov 19 18:15:31 2008 +0100
    18.2 +++ b/src/Pure/pure_thy.ML	Thu Nov 20 00:03:47 2008 +0100
    18.3 @@ -244,6 +244,9 @@
    18.4  val term = SimpleSyntax.read_term;
    18.5  val prop = SimpleSyntax.read_prop;
    18.6  
    18.7 +val typeT = Syntax.typeT;
    18.8 +val spropT = Syntax.spropT;
    18.9 +
   18.10  
   18.11  (* application syntax variants *)
   18.12  
   18.13 @@ -301,6 +304,7 @@
   18.14      ("",            typ "idt => pttrn",                Delimfix "_"),
   18.15      ("",            typ "pttrn => pttrns",             Delimfix "_"),
   18.16      ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
   18.17 +    ("",            typ "aprop => aprop",              Delimfix "'(_')"),
   18.18      ("",            typ "id => aprop",                 Delimfix "_"),
   18.19      ("",            typ "longid => aprop",             Delimfix "_"),
   18.20      ("",            typ "var => aprop",                Delimfix "_"),
   18.21 @@ -324,13 +328,16 @@
   18.22      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
   18.23      ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
   18.24      (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
   18.25 -    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))")]
   18.26 +    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
   18.27 +    ("Pure.term",   typ "logic => prop",               Delimfix "TERM _"),
   18.28 +    ("Pure.conjunction", typ "prop => prop => prop",   InfixrName ("&&&", 2))]
   18.29    #> Sign.add_syntax_i applC_syntax
   18.30    #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   18.31     [("fun",      typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   18.32      ("_bracket", typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   18.33      ("_ofsort",  typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
   18.34 -    ("_constrain", typ "'a => type => 'a",     Mixfix ("_\\<Colon>_", [4, 0], 3)),
   18.35 +    ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
   18.36 +    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
   18.37      ("_idtyp",    typ "id => type => idt",     Mixfix ("_\\<Colon>_", [], 0)),
   18.38      ("_idtypdummy", typ "type => idt",         Mixfix ("'_()\\<Colon>_", [], 0)),
   18.39      ("_type_constraint_", typ "'a",            NoSyn),
   18.40 @@ -342,9 +349,7 @@
   18.41      ("_bigimpl", typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   18.42      ("_DDDOT",   typ "logic",                  Delimfix "\\<dots>")]
   18.43    #> Sign.add_modesyntax_i ("", false)
   18.44 -   [("prop", typ "prop => prop", Mixfix ("_", [0], 0)),
   18.45 -    ("Pure.term", typ "'a => prop", Delimfix "TERM _"),
   18.46 -    ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))]
   18.47 +   [("prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   18.48    #> Sign.add_modesyntax_i ("HTML", false)
   18.49     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   18.50    #> Sign.add_consts_i
   18.51 @@ -372,7 +377,7 @@
   18.52      ("sort_constraint_def",
   18.53        prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
   18.54        \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
   18.55 -    ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   18.56 +    ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
   18.57    #> Sign.hide_const false "Pure.term"
   18.58    #> Sign.hide_const false "Pure.sort_constraint"
   18.59    #> Sign.hide_const false "Pure.conjunction"