HTML output;
authorwenzelm
Wed Mar 10 10:55:12 1999 +0100 (1999-03-10)
changeset 63407d5cbd5819a0
parent 6339 b995ab768117
child 6341 3b0b5890e1f1
HTML output;
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/HOL/Prod.thy
src/HOL/TLA/Intensional.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/ZF/ZF.thy
     1.1 --- a/src/FOL/IFOL.thy	Wed Mar 10 10:53:53 1999 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Wed Mar 10 10:55:12 1999 +0100
     1.3 @@ -67,6 +67,10 @@
     1.4    "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
     1.5    "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  Not           :: o => o                       ("\\<not> _" [40] 40)
     1.9 +
    1.10 +
    1.11  local
    1.12  
    1.13  rules
     2.1 --- a/src/HOL/HOL.thy	Wed Mar 10 10:53:53 1999 +0100
     2.2 +++ b/src/HOL/HOL.thy	Wed Mar 10 10:55:12 1999 +0100
     2.3 @@ -140,10 +140,13 @@
     2.4    "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
     2.5    "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
     2.6  
     2.7 -
     2.8  syntax (xsymbols)
     2.9    "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
    2.10  
    2.11 +syntax (HTML output)
    2.12 +  Not           :: bool => bool                     ("\\<not> _" [40] 40)
    2.13 +
    2.14 +
    2.15  (** Rules and definitions **)
    2.16  
    2.17  local
     3.1 --- a/src/HOL/Prod.thy	Wed Mar 10 10:53:53 1999 +0100
     3.2 +++ b/src/HOL/Prod.thy	Wed Mar 10 10:55:12 1999 +0100
     3.3 @@ -27,6 +27,9 @@
     3.4  syntax (symbols)
     3.5    "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
     3.6  
     3.7 +syntax (HTML output)
     3.8 +  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
     3.9 +
    3.10  
    3.11  (* abstract constants and syntax *)
    3.12  
     4.1 --- a/src/HOL/TLA/Intensional.thy	Wed Mar 10 10:53:53 1999 +0100
     4.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Mar 10 10:55:12 1999 +0100
     4.3 @@ -161,6 +161,9 @@
     4.4    "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
     4.5    "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
     4.6  
     4.7 +syntax (HTML output)
     4.8 +  "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
     4.9 +
    4.10  rules
    4.11    Valid_def   "|- A    ==  ALL w. w |= A"
    4.12  
    4.13 @@ -173,5 +176,3 @@
    4.14    unl_Rex     "w |= ? x. A x  ==  ? x. (w |= A x)"
    4.15    unl_Rex1    "w |= ?! x. A x  ==  ?! x. (w |= A x)"
    4.16  end
    4.17 -
    4.18 -ML
     5.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Mar 10 10:53:53 1999 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Mar 10 10:55:12 1999 +0100
     5.3 @@ -41,6 +41,9 @@
     5.4  syntax (symbols)
     5.5    "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
     5.6  
     5.7 +syntax (HTML output)
     5.8 +  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
     5.9 +
    5.10  
    5.11  defs
    5.12  
     6.1 --- a/src/ZF/ZF.thy	Wed Mar 10 10:53:53 1999 +0100
     6.2 +++ b/src/ZF/ZF.thy	Wed Mar 10 10:55:12 1999 +0100
     6.3 @@ -164,6 +164,9 @@
     6.4    "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
     6.5  *)
     6.6  
     6.7 +syntax (HTML output)
     6.8 +  "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
     6.9 +
    6.10  
    6.11  defs
    6.12