equal
deleted
inserted
replaced
9 |
9 |
10 nominal_datatype lam = |
10 nominal_datatype lam = |
11 Var "name" |
11 Var "name" |
12 | App "lam" "lam" |
12 | App "lam" "lam" |
13 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
13 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
14 |
|
15 ML {* Method.SIMPLE_METHOD' *} |
|
16 ML {* Sign.intern_const *} |
|
17 |
|
18 ML {* |
|
19 val test:((Proof.context -> Method.method) context_parser) = |
|
20 Scan.succeed (fn ctxt => |
|
21 let |
|
22 val _ = Inductive.the_inductive ctxt "local.frees_lst_graph" |
|
23 in |
|
24 Method.SIMPLE_METHOD' (K (all_tac)) |
|
25 end) |
|
26 *} |
|
27 |
|
28 method_setup test = {* test *} {* test *} |
|
29 |
14 |
30 section {* Simple examples from Norrish 2004 *} |
15 section {* Simple examples from Norrish 2004 *} |
31 |
16 |
32 nominal_primrec |
17 nominal_primrec |
33 is_app :: "lam \<Rightarrow> bool" |
18 is_app :: "lam \<Rightarrow> bool" |