--- a/ex/PL.thy Fri Jul 08 17:22:58 1994 +0200
+++ b/ex/PL.thy Fri Jul 08 17:39:02 1994 +0200
@@ -6,7 +6,9 @@
Inductive definition of propositional logic.
*)
-PL = Finite + PL0 +
+PL = Finite +
+datatype
+ 'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90)
consts
axK,axS,axDN:: "'a pl set"
ruleMP,thms :: "'a pl set => 'a pl set"
@@ -40,6 +42,6 @@
eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)"
hyps_def
- "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)"
+ "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)"
end