equal
deleted
inserted
replaced
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
17 thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list |
18 end |
18 end |
19 |
19 |
20 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
20 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
21 struct |
21 struct |
22 |
|
23 fun lookup xs x = the (AList.lookup (op=) xs x) |
|
24 |
22 |
25 (* supports lemmas for constructors *) |
23 (* supports lemmas for constructors *) |
26 |
24 |
27 fun mk_supports_goal ctxt qtrm = |
25 fun mk_supports_goal ctxt qtrm = |
28 let |
26 let |