same_append_eq / append_same_eq are now used for simplifying induction rules.
header {* Plain HOL *}theory Plainimports Datatype Record FunDef Extractionbegintext {* Plain bootstrap of fundamental HOL tools and packages; does not include @{text Hilbert_Choice}.*}ML {* path_add "~~/src/HOL/Library" *}end