equal
deleted
inserted
replaced
21 |
21 |
22 declare F_strict [simp] K [simp] |
22 declare F_strict [simp] K [simp] |
23 |
23 |
24 lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))" |
24 lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))" |
25 apply (simplesubst H) |
25 apply (simplesubst H) |
26 apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *}) |
26 apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *}) |
27 apply (simp (no_asm)) |
27 apply (simp (no_asm)) |
28 apply (simp (no_asm_simp) split: COND_cases_iff) |
28 apply (simp (no_asm_simp) split: COND_cases_iff) |
29 done |
29 done |
30 |
30 |
31 end |
31 end |