changeset 63435 | 7743df69a6b4 |
parent 60770 | 240563fbf41d |
--- a/src/ZF/Inductive_ZF.thy Mon Jul 11 10:43:54 2016 +0200 +++ b/src/ZF/Inductive_ZF.thy Mon Jul 11 11:15:10 2016 +0200 @@ -16,7 +16,7 @@ keywords "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and "domains" "intros" "monos" "con_defs" "type_intros" "type_elims" - "elimination" "induction" "case_eqns" "recursor_eqns" + "elimination" "induction" "case_eqns" "recursor_eqns" :: quasi_command begin lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"