src/HOL/Induct/PropLog.thy
 changeset 39246 9e58f0499f57 parent 36862 952b2b102a0a child 45605 a89b4bc311a5
```--- a/src/HOL/Induct/PropLog.thy	Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Induct/PropLog.thy	Wed Sep 08 19:21:46 2010 +0200
@@ -41,25 +41,20 @@

subsubsection {* Semantics of propositional logic. *}

-consts
-  eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)
-
-primrec     "tt[[false]] = False"
-            "tt[[#v]]    = (v \<in> tt)"
-  eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
+primrec eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100) where
+            "tt[[false]] = False"
+|            "tt[[#v]]    = (v \<in> tt)"
+| eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"

text {*
A finite set of hypotheses from @{text t} and the @{text Var}s in
@{text p}.
*}

-consts
-  hyps  :: "['a pl, 'a set] => 'a pl set"
-
-primrec
+primrec hyps  :: "['a pl, 'a set] => 'a pl set" where
"hyps false  tt = {}"
-  "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
-  "hyps (p->q) tt = hyps p tt Un hyps q tt"
+| "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
+| "hyps (p->q) tt = hyps p tt Un hyps q tt"

subsubsection {* Logical consequence *}
```