equal
deleted
inserted
replaced
1041 *} |
1041 *} |
1042 |
1042 |
1043 (* 1. conversion (is not a pattern) *) |
1043 (* 1. conversion (is not a pattern) *) |
1044 thm lambda_prs |
1044 thm lambda_prs |
1045 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) |
1045 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) |
|
1046 (* prservation lemma *) |
1046 (* and simplification with *) |
1047 (* and simplification with *) |
1047 thm all_prs ex_prs |
1048 thm all_prs ex_prs |
1048 (* 3. simplification with *) |
1049 (* 3. simplification with *) |
1049 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1050 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1050 (* 4. Test for refl *) |
1051 (* 4. Test for refl *) |
1051 |
1052 |
1052 ML {* |
1053 ML {* |
1053 fun clean_tac lthy = |
1054 fun clean_tac lthy = |
1054 let |
1055 let |