merged
authornipkow
Fri Dec 21 10:08:06 2012 +0100 (2012-12-21)
changeset 50612def80e410f3b
parent 50600 48c0c3bc40dd
parent 50605 620515b73a77
child 50613 168befd6cfa6
merged
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Thu Dec 20 09:49:00 2012 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Fri Dec 21 10:08:06 2012 +0100
     1.3 @@ -590,30 +590,38 @@
     1.4  \section*{Infix operators in Main} % @{theory Main}
     1.5  
     1.6  \begin{center}
     1.7 -\begin{tabular}{lll}
     1.8 -Operator & precedence & associativity \\
     1.9 -@{text"="}, @{text"\<noteq>"} & 50 & left\\
    1.10 -@{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
    1.11 -@{text"\<and>"} & 35 & right \\
    1.12 -@{text"\<or>"} & 30 & right \\
    1.13 -@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
    1.14 -@{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
    1.15 -@{text"\<in>"}, @{text"\<notin>"} & 50 \\
    1.16 -@{text"\<inter>"} & 70 & left \\
    1.17 -@{text"\<union>"} & 65 & left \\
    1.18 -@{text"\<circ>"} & 55 & left\\
    1.19 -@{text"`"} & 90 & right\\
    1.20 -@{text"O"} & 75 & right\\
    1.21 -@{text"``"} & 90 & right\\
    1.22 -@{text"+"}, @{text"-"} & 65 & left \\
    1.23 -@{text"*"}, @{text"/"} & 70 & left \\
    1.24 -@{text"div"}, @{text"mod"} & 70 & left\\
    1.25 -@{text"^"} & 80 & right\\
    1.26 -@{text"^^"} & 80 & right\\
    1.27 -@{text"dvd"} & 50 \\
    1.28 -@{text"#"}, @{text"@"} & 65 & right\\
    1.29 -@{text"!"} & 100 & left\\
    1.30 -@{text"++"} & 100 & left\\
    1.31 +\begin{tabular}{llll}
    1.32 + & Operator & precedence & associativity \\
    1.33 +\hline
    1.34 +Meta-logic & @{text"\<Longrightarrow>"} & 1 & right \\
    1.35 +& @{text"\<equiv>"} & 2 \\
    1.36 +\hline
    1.37 +Logic & @{text"\<and>"} & 35 & right \\
    1.38 +&@{text"\<or>"} & 30 & right \\
    1.39 +&@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
    1.40 +&@{text"="}, @{text"\<noteq>"} & 50 & left\\
    1.41 +\hline
    1.42 +Orderings & @{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
    1.43 +\hline
    1.44 +Sets & @{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
    1.45 +&@{text"\<in>"}, @{text"\<notin>"} & 50 \\
    1.46 +&@{text"\<inter>"} & 70 & left \\
    1.47 +&@{text"\<union>"} & 65 & left \\
    1.48 +\hline
    1.49 +Functions and Relations & @{text"\<circ>"} & 55 & left\\
    1.50 +&@{text"`"} & 90 & right\\
    1.51 +&@{text"O"} & 75 & right\\
    1.52 +&@{text"``"} & 90 & right\\
    1.53 +\hline
    1.54 +Numbers & @{text"+"}, @{text"-"} & 65 & left \\
    1.55 +&@{text"*"}, @{text"/"} & 70 & left \\
    1.56 +&@{text"div"}, @{text"mod"} & 70 & left\\
    1.57 +&@{text"^"} & 80 & right\\
    1.58 +&@{text"^^"} & 80 & right\\
    1.59 +&@{text"dvd"} & 50 \\
    1.60 +\hline
    1.61 +Lists & @{text"#"}, @{text"@"} & 65 & right\\
    1.62 +&@{text"!"} & 100 & left
    1.63  \end{tabular}
    1.64  \end{center}
    1.65  *}
     2.1 --- a/src/Pure/Pure.thy	Thu Dec 20 09:49:00 2012 +0100
     2.2 +++ b/src/Pure/Pure.thy	Fri Dec 21 10:08:06 2012 +0100
     2.3 @@ -146,7 +146,7 @@
     2.4  qed
     2.5  
     2.6  lemma imp_conjunction:
     2.7 -  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
     2.8 +  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
     2.9  proof
    2.10    assume conj: "PROP A ==> PROP B &&& PROP C"
    2.11    show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
     3.1 --- a/src/Pure/pure_thy.ML	Thu Dec 20 09:49:00 2012 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Fri Dec 21 10:08:06 2012 +0100
     3.3 @@ -177,7 +177,7 @@
     3.4    #> Sign.add_modesyntax_i ("HTML", false)
     3.5     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
     3.6    #> Sign.add_consts_i
     3.7 -   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
     3.8 +   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
     3.9      (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    3.10      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    3.11      (Binding.name "prop", typ "prop => prop", NoSyn),