Mercurial Mercurial > repos > Old_HOL / annotate
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.
ex/PL0.thy
author clasohm
Fri, 17 Jun 1994 14:16:50 +0200
changeset 81 fded09018308
parent 56 385d51d74f71
child 91 a94029edb01f
permissions -rw-r--r--
adopted to new datatype definition method
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56
385d51d74f71 Used Datatype functor to define propositional logic terms.
nipkow
parents:
diff changeset 
     1
 
(*  Title: 	HOL/ex/pl0.thy
385d51d74f71 Used Datatype functor to define propositional logic terms.
nipkow
parents:
diff changeset 
     2
 
    ID:         $Id$
385d51d74f71 Used Datatype functor to define propositional logic terms.
nipkow
parents:
diff changeset 
     3
 
    Author: 	Tobias Nipkow
385d51d74f71 Used Datatype functor to define propositional logic terms.
nipkow
parents:
diff changeset 
     4
 
    Copyright   1994  TU Muenchen
385d51d74f71 Used Datatype functor to define propositional logic terms.
nipkow
parents:
diff changeset 
     5
 












385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




     6


Syntax of propositional logic formulae.













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




     7


*)













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




     8














385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




     9


PL0 = HOL +













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    10


types 'a pl













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    11


arities pl :: (term)term













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    12


consts













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    13


    false	:: "'a pl"













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    14


    "->"	:: "['a pl,'a pl] => 'a pl"	(infixr 90)













385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    15


    var		:: "'a => 'a pl"		("#_")








81






fded09018308
adopted to new datatype definition method



clasohm


parents: 
56

diff
changeset




    16


datatype













fded09018308
adopted to new datatype definition method



clasohm


parents: 
56

diff
changeset




    17


    'a pl = false | var('a) | "op->" ('a pl,'a pl)








56






385d51d74f71
Used Datatype functor to define propositional logic terms.



nipkow


parents: 

diff
changeset




    18


end















Old_HOL