Changes

Summary

more 'corec' docs
tuning
more 'corec' docs
try tactics in right order w.r.t. schematics
more natural order for 'cong_intros'
more 'corec' documentation
renamed generated theorem
tuning
added sketchy 'corec' documentation

Changeset 62747:f65ef4723aca by blanchet: more 'corec' docs
The file was modified	`src/Doc/Corec/Corec.thy` (diff)
The file was modified	`src/Doc/Corec/document/root.tex` (diff)
The file was modified	`src/Doc/Datatypes/Datatypes.thy` (diff)
The file was modified	`src/Doc/Datatypes/document/root.tex` (diff)
Changeset 62746:4384baae8753 by blanchet: tuning
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML` (diff)
Changeset 62745:257a022f7e7b by blanchet: more 'corec' docs
The file was modified	`src/Doc/Corec/Corec.thy` (diff)
Changeset 62744:b4f139bf02e3 by blanchet: try tactics in right order w.r.t. schematics
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML` (diff)
Changeset 62743:f9a65b48f5e2 by blanchet: more natural order for 'cong_intros'
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML` (diff)
Changeset 62742:bfb5a70e4319 by blanchet: more 'corec' documentation
The file was modified	`src/Doc/Corec/Corec.thy` (diff)
The file was modified	`src/Doc/Corec/document/root.tex` (diff)
The file was modified	`src/Doc/manual.bib` (diff)
Changeset 62741:1ddfe28117e9 by blanchet: renamed generated theorem
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML` (diff)
Changeset 62740:69e4a4fffea9 by blanchet: tuning
The file was modified	`src/Doc/Datatypes/Datatypes.thy` (diff)
Changeset 62739:628c97d39627 by blanchet: added sketchy 'corec' documentation
The file was added	`src/Doc/Corec/Corec.thy`
The file was added	`src/Doc/Corec/document/build`
The file was added	`src/Doc/Corec/document/root.tex`
The file was added	`src/Doc/Corec/document/style.sty`
The file was modified	`doc/Contents` (diff)
The file was modified	`src/Doc/ROOT` (diff)