theory Term8+
−
imports "../NewParser"+
−
begin+
−
+
−
(* example 8 *)+
−
+
−
atom_decl name+
−
+
−
ML {* val _ = cheat_alpha_bn_rsp := true *}+
−
+
−
nominal_datatype foo =+
−
  Foo0 "name"+
−
| Foo1 b::"bar" f::"foo" bind_set "bv b" in f+
−
and bar =+
−
  Bar0 "name"+
−
| Bar1 "name" s::"name" b::"bar" bind_set s in b+
−
binder+
−
  bv+
−
where+
−
  "bv (Bar0 x) = {}"+
−
| "bv (Bar1 v x b) = {atom v}"+
−
+
−
thm foo_bar.supp+
−
+
−
end+
−
+
−
+
−