Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"
authorblanchet
Tue, 03 Mar 2015 16:37:45 +0100
changeset 59578 5f56d4ff6635
parent 59577 012c6165bbd2
child 59579 d8fff0b94c53
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"
src/HOL/Tools/BNF/bnf_lfp_size.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 16:37:45 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 03 16:37:45 2015 +0100
@@ -65,7 +65,7 @@
   unfold_thms_tac ctxt [size_def] THEN
   HEADGOAL (rtac (rec_o_map RS trans) THEN'
     asm_simp_tac (ss_only (inj_maps @ size_maps @ size_gen_o_map_simps) ctxt)) THEN
-  IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
+  IF_UNSOLVED (unfold_thms_tac ctxt @{thms id_def o_def} THEN HEADGOAL (rtac refl));
 
 fun mk_size_neq ctxt cts exhaust sizes =
   HEADGOAL (rtac (Ctr_Sugar_Util.cterm_instantiate_pos (map SOME cts) exhaust)) THEN
isabelle