summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 4207 | 061919f8da9c |

parent 4189 | b8c7a6bc6c16 |

child 4269 | a045600f0c98 |

1.1 --- a/NEWS Wed Nov 12 12:34:43 1997 +0100 1.2 +++ b/NEWS Wed Nov 12 12:38:12 1997 +0100 1.3 @@ -95,7 +95,7 @@ 1.4 1.5 *** HOL *** 1.6 1.7 -* HOL: there is a new splitter `split_prem_tac' that can be used e.g. 1.8 +* HOL: there is a new splitter `split_asm_tac' that can be used e.g. 1.9 with `addloop' of the simplifier to faciliate case splitting in premises. 1.10 1.11 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions; 1.12 @@ -131,7 +131,7 @@ 1.13 expand_list_case and expand_option_case have been renamed to 1.14 split_list_case and split_option_case. 1.15 1.16 - Additionally, there is a theorem `split_t_case_prem' of the form 1.17 + Additionally, there is a theorem `split_t_case_asm' of the form 1.18 1.19 P(t_case f1 ... fn x) = 1.20 ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) | 1.21 @@ -139,7 +139,7 @@ 1.22 (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) 1.23 ) 1.24 1.25 - it be used with the new `split_prem_tac'. 1.26 + it be used with the new `split_asm_tac'. 1.27 1.28 * HOL/Lists: the function "set_of_list" has been renamed "set" 1.29 (and its theorems too); 1.30 @@ -175,7 +175,7 @@ 1.31 1.32 *** FOL and ZF *** 1.33 1.34 -* FOL: there is a new splitter `split_prem_tac' that can be used e.g. 1.35 +* FOL: there is a new splitter `split_asm_tac' that can be used e.g. 1.36 with `addloop' of the simplifier to faciliate case splitting in premises. 1.37 1.38 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as