src/FOLP/IFOLP.thy
changeset 41310 65631ca437c9
parent 39557 fe5722fce758
child 42616 92715b528e78
     1.1 --- a/src/FOLP/IFOLP.thy	Mon Dec 20 15:24:25 2010 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Mon Dec 20 16:44:33 2010 +0100
     1.3 @@ -24,14 +24,14 @@
     1.4   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
     1.5  
     1.6        (*** Logical Connectives -- Type Formers ***)
     1.7 - "op ="         ::      "['a,'a] => o"  (infixl "=" 50)
     1.8 + eq             ::      "['a,'a] => o"  (infixl "=" 50)
     1.9   True           ::      "o"
    1.10   False          ::      "o"
    1.11   Not            ::      "o => o"        ("~ _" [40] 40)
    1.12 - "op &"         ::      "[o,o] => o"    (infixr "&" 35)
    1.13 - "op |"         ::      "[o,o] => o"    (infixr "|" 30)
    1.14 - "op -->"       ::      "[o,o] => o"    (infixr "-->" 25)
    1.15 - "op <->"       ::      "[o,o] => o"    (infixr "<->" 25)
    1.16 + conj           ::      "[o,o] => o"    (infixr "&" 35)
    1.17 + disj           ::      "[o,o] => o"    (infixr "|" 30)
    1.18 + imp            ::      "[o,o] => o"    (infixr "-->" 25)
    1.19 + iff            ::      "[o,o] => o"    (infixr "<->" 25)
    1.20        (*Quantifiers*)
    1.21   All            ::      "('a => o) => o"        (binder "ALL " 10)
    1.22   Ex             ::      "('a => o) => o"        (binder "EX " 10)
    1.23 @@ -51,9 +51,9 @@
    1.24   inr            :: "p=>p"
    1.25   when           :: "[p, p=>p, p=>p]=>p"
    1.26   lambda         :: "(p => p) => p"      (binder "lam " 55)
    1.27 - "op `"         :: "[p,p]=>p"           (infixl "`" 60)
    1.28 + App            :: "[p,p]=>p"           (infixl "`" 60)
    1.29   alll           :: "['a=>p]=>p"         (binder "all " 55)
    1.30 - "op ^"         :: "[p,'a]=>p"          (infixl "^" 55)
    1.31 + app            :: "[p,'a]=>p"          (infixl "^" 55)
    1.32   exists         :: "['a,p]=>p"          ("(1[_,/_])")
    1.33   xsplit         :: "[p,['a,p]=>p]=>p"
    1.34   ideq           :: "'a=>p"
    1.35 @@ -595,7 +595,7 @@
    1.36  struct
    1.37    (*Take apart an equality judgement; otherwise raise Match!*)
    1.38    fun dest_eq (Const (@{const_name Proof}, _) $
    1.39 -    (Const (@{const_name "op ="}, _)  $ t $ u) $ _) = (t, u);
    1.40 +    (Const (@{const_name eq}, _)  $ t $ u) $ _) = (t, u);
    1.41  
    1.42    val imp_intr = @{thm impI}
    1.43