equal
deleted
inserted
replaced
1049 (* 1. folding of definitions and preservation lemmas; *) |
1049 (* 1. folding of definitions and preservation lemmas; *) |
1050 (* and simplification with *) |
1050 (* and simplification with *) |
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 |
|
1057 (* 4. simplification with *) |
1056 thm Quotient_abs_rep Quotient_rel_rep id_simps |
1058 thm Quotient_abs_rep Quotient_rel_rep id_simps |
1057 (* 4. Test for refl *) |
1059 (* 5. Test for refl *) |
1058 |
1060 |
1059 ML {* |
1061 ML {* |
1060 fun clean_tac lthy = |
1062 fun clean_tac lthy = |
1061 let |
1063 let |
1062 val thy = ProofContext.theory_of lthy; |
1064 val thy = ProofContext.theory_of lthy; |