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 po_refl_iff_T = make_iff_T po_refl; |
|
14 |
|
15 val CCL_ss = FOL_ss addcongs set_congs |
13 val CCL_ss = FOL_ss addcongs set_congs |
16 addsimps ([po_refl_iff_T] @ mem_rews); |
14 addsimps ([po_refl RS P_iff_T] @ mem_rews); |
17 |
15 |
18 (*** Congruence Rules ***) |
16 (*** Congruence Rules ***) |
19 |
17 |
20 (*similar to AP_THM in Gordon's HOL*) |
18 (*similar to AP_THM in Gordon's HOL*) |
21 val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" |
19 val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" |