equal
deleted
inserted
replaced
34 [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim}, |
34 [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim}, |
35 @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]); |
35 @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]); |
36 |
36 |
37 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; |
37 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; |
38 |
38 |
39 val perm_bool = mk_meta_eq @{thm perm_bool}; |
39 val perm_bool = mk_meta_eq @{thm perm_bool_def}; |
40 val perm_boolI = @{thm perm_boolI}; |
40 val perm_boolI = @{thm perm_boolI}; |
41 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb |
41 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb |
42 (Drule.strip_imp_concl (cprop_of perm_boolI)))); |
42 (Drule.strip_imp_concl (cprop_of perm_boolI)))); |
43 |
43 |
44 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate |
44 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate |