equal
deleted
inserted
replaced
56 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get; |
56 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get; |
57 |
57 |
58 val get_eqvts_thms = eqvts o Context.Proof; |
58 val get_eqvts_thms = eqvts o Context.Proof; |
59 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
59 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
60 |
60 |
61 val add_thm = EqvtData.map o Item_Net.update; |
61 fun checked_update key net = |
|
62 (if Item_Net.member net key then |
|
63 warning "Theorem already declared as equivariant." |
|
64 else (); |
|
65 Item_Net.update key net) |
|
66 |
|
67 val add_thm = EqvtData.map o checked_update; |
62 val del_thm = EqvtData.map o Item_Net.remove; |
68 val del_thm = EqvtData.map o Item_Net.remove; |
63 |
69 |
64 fun add_raw_thm thm = |
70 fun add_raw_thm thm = |
65 case prop_of thm of |
71 case prop_of thm of |
66 Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) |
72 Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) |