equal
deleted
inserted
replaced
3317 shows "Fresh h = h a" |
3317 shows "Fresh h = h a" |
3318 apply (rule Fresh_apply) |
3318 apply (rule Fresh_apply) |
3319 apply (auto simp add: fresh_Pair intro: a) |
3319 apply (auto simp add: fresh_Pair intro: a) |
3320 done |
3320 done |
3321 |
3321 |
3322 lemma "1 = 1 &&& 2 = 2" |
|
3323 apply(tactic {* ALLGOALS (asm_full_simp_tac @{simpset}) *}) |
|
3324 done |
|
3325 |
|
3326 |
|
3327 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm => |
3322 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm => |
3328 let |
3323 let |
3329 val ctxt = Simplifier.the_context ss |
3324 val ctxt = Simplifier.the_context ss |
3330 val _ $ h = term_of ctrm |
3325 val _ $ h = term_of ctrm |
3331 |
3326 |