equal
deleted
inserted
replaced
1051 thm babs_prs all_prs ex_prs |
1051 thm babs_prs all_prs ex_prs |
1052 (* 2. unfolding of ---> in front of everything, except *) |
1052 (* 2. unfolding of ---> in front of everything, except *) |
1053 (* bound variables *) |
1053 (* bound variables *) |
1054 thm fun_map.simps |
1054 thm fun_map.simps |
1055 (* 3. simplification with *) |
1055 (* 3. simplification with *) |
1056 lambda_prs |
1056 thm lambda_prs |
1057 (* 4. simplification with *) |
1057 (* 4. simplification with *) |
1058 thm Quotient_abs_rep Quotient_rel_rep id_simps |
1058 thm Quotient_abs_rep Quotient_rel_rep id_simps |
1059 (* 5. Test for refl *) |
1059 (* 5. Test for refl *) |
1060 |
1060 |
1061 ML {* |
1061 ML {* |