equal
deleted
inserted
replaced
139 | BP1 "bp1" "bp1" |
139 | BP1 "bp1" "bp1" |
140 binder |
140 binder |
141 bv1 |
141 bv1 |
142 where |
142 where |
143 "bv1 (BUnit1) = {}" |
143 "bv1 (BUnit1) = {}" |
|
144 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
144 | "bv1 (BV1 x) = {atom x}" |
145 | "bv1 (BV1 x) = {atom x}" |
145 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
146 |
146 |
147 |
147 thm bv1_raw.simps |
148 thm bv1_raw.simps |
148 |
149 |
149 (* example 2 from Terms.thy *) |
150 (* example 2 from Terms.thy *) |
150 |
151 |
336 and Cbinders :: "spec \<Rightarrow> atom set" |
337 and Cbinders :: "spec \<Rightarrow> atom set" |
337 where |
338 where |
338 "cbinders (Type t T) = {atom t}" |
339 "cbinders (Type t T) = {atom t}" |
339 | "cbinders (Dty t) = {atom t}" |
340 | "cbinders (Dty t) = {atom t}" |
340 | "cbinders (DStru x s) = {atom x}" |
341 | "cbinders (DStru x s) = {atom x}" |
341 | "cbinders (Val v M) = {atom v}" |
342 | "cbinders (Val v M) = {atom v}"*) |
342 | "Cbinders (Type1 t) = {atom t}" |
343 | "Cbinders (Type1 t) = {atom t}" |
343 | "Cbinders (Type2 t T) = {atom t}" |
344 | "Cbinders (Type2 t T) = {atom t}" |
344 | "Cbinders (SStru x S) = {atom x}" |
345 | "Cbinders (SStru x S) = {atom x}" |
345 | "Cbinders (SVal v T) = {atom v}" |
346 | "Cbinders (SVal v T) = {atom v}" |
|
347 |
346 |
348 |
347 (* core haskell *) |
349 (* core haskell *) |
348 print_theorems |
350 print_theorems |
349 |
351 |
350 atom_decl var |
352 atom_decl var |