Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/ILL_predlog.thy
changeset 22895 adc529c89281
parent 21427 7c8f4a331f9b
child 35054 a5db9779b026
equal deleted inserted replaced
22894:619b270607ac 22895:adc529c89281 
     9 consts
 
     9 consts
 
    10   conj :: "[plf,plf] => plf"   (infixr "&" 35)
 
    10   conj :: "[plf,plf] => plf"   (infixr "&" 35)
 
    11   disj :: "[plf,plf] => plf"   (infixr "|" 35)
 
    11   disj :: "[plf,plf] => plf"   (infixr "|" 35)
 
    12   impl :: "[plf,plf] => plf"   (infixr ">" 35)
 
    12   impl :: "[plf,plf] => plf"   (infixr ">" 35)
 
    13   eq :: "[plf,plf] => plf"   (infixr "=" 35)
 
    13   eq :: "[plf,plf] => plf"   (infixr "=" 35)
 
    14   "@NG" :: "plf => plf"   ("- _ " [50] 55)
 
       
    15   ff    :: "plf"
 
    14   ff    :: "plf"
 
    16 
    15 
    17   PL    :: "plf => o"      ("[* / _ / *]" [] 100)
 
    16   PL    :: "plf => o"      ("[* / _ / *]" [] 100)
 
       
    17 
       
    18 syntax
 
       
    19   "_NG" :: "plf => plf"   ("- _ " [50] 55)
 
    18 
    20 
    19 translations
 
    21 translations
 
    20 
    22 
    21   "[* A & B *]" == "[*A*] && [*B*]"
 
    23   "[* A & B *]" == "[*A*] && [*B*]"
 
    22   "[* A | B *]" == "![*A*] ++ ![*B*]"
 
    24   "[* A | B *]" == "![*A*] ++ ![*B*]"
isabelle