equal
deleted
inserted
replaced
8 |
8 |
9 open CCL; |
9 open CCL; |
10 |
10 |
11 val ccl_data_defs = [apply_def,fix_def]; |
11 val ccl_data_defs = [apply_def,fix_def]; |
12 |
12 |
13 val CCL_ss = FOL_ss addcongs set_congs |
13 val CCL_ss = set_ss addsimps [po_refl RS P_iff_T]; |
14 addsimps ([po_refl RS P_iff_T] @ mem_rews); |
|
15 |
14 |
16 (*** Congruence Rules ***) |
15 (*** Congruence Rules ***) |
17 |
16 |
18 (*similar to AP_THM in Gordon's HOL*) |
17 (*similar to AP_THM in Gordon's HOL*) |
19 qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" |
18 qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" |