--- a/src/HOL/BNF/Examples/Misc_Codata.thy Thu Jun 06 15:56:17 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codata.thy Thu Jun 06 21:12:08 2013 +0200
@@ -1,7 +1,8 @@
(* Title: HOL/BNF/Examples/Misc_Codata.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
- Copyright 2012
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012, 2013
Miscellaneous codatatype declarations.
*)
@@ -16,6 +17,8 @@
codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit
+codatatype simple'' = X1'' nat int | X2''
+
codatatype 'a stream = Stream 'a "'a stream"
codatatype 'a mylist = MyNil | MyCons 'a "'a mylist"
--- a/src/HOL/BNF/Examples/Misc_Data.thy Thu Jun 06 15:56:17 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy Thu Jun 06 21:12:08 2013 +0200
@@ -17,6 +17,8 @@
datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit
+datatype_new simple'' = X1'' nat int | X2''
+
datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
datatype_new ('b, 'c, 'd, 'e) some_passive =
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Jun 06 15:56:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Jun 06 21:12:08 2013 +0200
@@ -161,7 +161,8 @@
(atac ORELSE' REPEAT o etac conjE THEN'
full_simp_tac
(ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN_MAYBE'
- REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
+ (REPEAT o etac conjE THEN' REPEAT o hyp_subst_tac ctxt) THEN'
+ REPEAT o rtac conjI THEN' REPEAT o rtac refl);
fun mk_coinduct_distinct_ctrs ctxt discs discs' =
hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'