Changes

Summary

emphasize dedicated rewrite rules for congruences
moved and exported tactic
export ML function (towards nonuniform datatypes)
generalized ML function (towards nonuniform datatypes)
generalized ML function (towards nonuniform datatypes)
merge
renamed confusing variable names

Changeset 64630:96015aecfeba by haftmann: emphasize dedicated rewrite rules for congruences
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/Statespace/state_fun.ML` (diff)
The file was modified	`src/HOL/String.thy` (diff)
Changeset 64629:a331208010b6 by blanchet: moved and exported tactic
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_tactics.ML` (diff)
Changeset 64628:19bc22274cd9 by blanchet: export ML function (towards nonuniform datatypes)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML` (diff)
Changeset 64627:8d7cb22482e3 by blanchet: generalized ML function (towards nonuniform datatypes)
The file was modified	`src/HOL/Tools/BNF/bnf_def.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar.ML` (diff)
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_sugar_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_countable.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML` (diff)
Changeset 64626:f6d0578b46c9 by blanchet: generalized ML function (towards nonuniform datatypes)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar.ML` (diff)
Changeset 64625:c6330e16743f by blanchet: merge
Changeset 64624:f3f457535fe2 by blanchet: renamed confusing variable names
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML` (diff)