equal
deleted
inserted
replaced
76 |
76 |
77 open FOLP_Simp; |
77 open FOLP_Simp; |
78 |
78 |
79 val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}]; |
79 val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}]; |
80 |
80 |
81 val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; |
81 val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews; |
82 |
82 |
83 |
83 |
84 val FOLP_rews = IFOLP_rews @ @{thms cla_rews}; |
84 val FOLP_rews = IFOLP_rews @ @{thms cla_rews}; |
85 |
85 |
86 val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; |
86 val FOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) FOLP_rews; |