equal
deleted
inserted
replaced
7 By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored |
7 By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored |
8 in a data-slot in the context. Possible modifiers |
8 in a data-slot in the context. Possible modifiers |
9 are [attribute add] and [attribute del] for adding and deleting, |
9 are [attribute add] and [attribute del] for adding and deleting, |
10 respectively the lemma from the data-slot. |
10 respectively the lemma from the data-slot. |
11 *) |
11 *) |
|
12 |
|
13 fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE)); |
|
14 fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE)); |
12 |
15 |
13 signature NOMINAL_THMDECLS = |
16 signature NOMINAL_THMDECLS = |
14 sig |
17 sig |
15 val print_data: Proof.context -> unit |
18 val print_data: Proof.context -> unit |
16 val eqvt_add: attribute |
19 val eqvt_add: attribute |
73 |
76 |
74 fun tactic (msg,tac) = |
77 fun tactic (msg,tac) = |
75 if !NOMINAL_EQVT_DEBUG |
78 if !NOMINAL_EQVT_DEBUG |
76 then (EVERY [tac, print_tac ("after "^msg)]) |
79 then (EVERY [tac, print_tac ("after "^msg)]) |
77 else tac |
80 else tac |
78 |
|
79 fun dynamic_thms thy name = PureThy.get_thms thy (Name name) |
|
80 |
81 |
81 fun tactic_eqvt ctx orig_thm pi typi = |
82 fun tactic_eqvt ctx orig_thm pi typi = |
82 let |
83 let |
83 val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
84 val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
84 val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |
85 val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |