equal
deleted
inserted
replaced
123 |
123 |
124 fun MaxSimpTac var_names tac = FIRST'[rtac subset_refl, set2pred_tac var_names THEN_MAYBE' tac]; |
124 fun MaxSimpTac var_names tac = FIRST'[rtac subset_refl, set2pred_tac var_names THEN_MAYBE' tac]; |
125 |
125 |
126 fun BasicSimpTac var_names tac = |
126 fun BasicSimpTac var_names tac = |
127 simp_tac |
127 simp_tac |
128 (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc]) |
128 (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc]) |
129 THEN_MAYBE' MaxSimpTac var_names tac; |
129 THEN_MAYBE' MaxSimpTac var_names tac; |
130 |
130 |
131 |
131 |
132 (** hoare_rule_tac **) |
132 (** hoare_rule_tac **) |
133 |
133 |