changeset 56 | 385d51d74f71 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/pl0.thy Tue Mar 22 08:28:31 1994 +0100 @@ -0,0 +1,16 @@ +(* Title: HOL/ex/pl0.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Syntax of propositional logic formulae. +*) + +PL0 = HOL + +types 'a pl +arities pl :: (term)term +consts + false :: "'a pl" + "->" :: "['a pl,'a pl] => 'a pl" (infixr 90) + var :: "'a => 'a pl" ("#_") +end