Changes

Summary

simp rules for fsts, snds, setl, setr
make predicator a first-class bnf citizen

Changeset 62325:7e4d31eefe60 by traytel: simp rules for fsts, snds, setl, setr
The file was modified	`src/HOL/BNF_Fixpoint_Base.thy` (diff)
Changeset 62324:ae44f16dcea5 by traytel: make predicator a first-class bnf citizen
The file was modified	`src/Doc/Datatypes/Datatypes.thy` (diff)
The file was modified	`src/HOL/BNF_Composition.thy` (diff)
The file was modified	`src/HOL/BNF_Def.thy` (diff)
The file was modified	`src/HOL/Basic_BNFs.thy` (diff)
The file was modified	`src/HOL/Cardinals/Bounded_Set.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set_Type.thy` (diff)
The file was modified	`src/HOL/Library/Dlist.thy` (diff)
The file was modified	`src/HOL/Library/FSet.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/bnf_axiomatization.ML` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_comp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_comp_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_def.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_def_tactics.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.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_compat.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lift.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_util.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_bnf.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer_bnf.ML` (diff)
The file was modified	`src/HOL/Transfer.thy` (diff)