equal
deleted
inserted
replaced
19 "bn (ANil) = []" |
19 "bn (ANil) = []" |
20 | "bn (ACons x t as) = (atom x) # (bn as)" |
20 | "bn (ACons x t as) = (atom x) # (bn as)" |
21 |
21 |
22 thm trm_assn.eq_iff |
22 thm trm_assn.eq_iff |
23 thm trm_assn.supp |
23 thm trm_assn.supp |
|
24 |
|
25 ML {* |
|
26 @{term Trueprop} ; |
|
27 @{const_name HOL.eq} |
|
28 *} |
24 |
29 |
25 thm trm_assn.fv_defs |
30 thm trm_assn.fv_defs |
26 thm trm_assn.eq_iff |
31 thm trm_assn.eq_iff |
27 thm trm_assn.bn_defs |
32 thm trm_assn.bn_defs |
28 thm trm_assn.perm_simps |
33 thm trm_assn.perm_simps |