ex/PL0.thy
author lcp
Thu, 21 Apr 1994 11:28:32 +0200
changeset 68 acad709cad5d
parent 56 385d51d74f71
child 81 fded09018308
permissions -rw-r--r--
tidied definitions and proofs
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"		("#_")
385d51d74f71 Used Datatype functor to define propositional logic terms.
nipkow
parents:
diff changeset
    16
end