equal
deleted
inserted
replaced
411 by blast |
411 by blast |
412 |
412 |
413 lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a" |
413 lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a" |
414 by auto |
414 by auto |
415 |
415 |
416 ML_file "Tools/inductive.ML" |
416 ML_file \<open>Tools/inductive.ML\<close> |
417 |
417 |
418 lemmas [mono] = |
418 lemmas [mono] = |
419 imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
419 imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
420 imp_mono not_mono |
420 imp_mono not_mono |
421 Ball_def Bex_def |
421 Ball_def Bex_def |
512 |
512 |
513 subsection \<open>Inductive datatypes and primitive recursion\<close> |
513 subsection \<open>Inductive datatypes and primitive recursion\<close> |
514 |
514 |
515 text \<open>Package setup.\<close> |
515 text \<open>Package setup.\<close> |
516 |
516 |
517 ML_file "Tools/Old_Datatype/old_datatype_aux.ML" |
517 ML_file \<open>Tools/Old_Datatype/old_datatype_aux.ML\<close> |
518 ML_file "Tools/Old_Datatype/old_datatype_prop.ML" |
518 ML_file \<open>Tools/Old_Datatype/old_datatype_prop.ML\<close> |
519 ML_file "Tools/Old_Datatype/old_datatype_data.ML" |
519 ML_file \<open>Tools/Old_Datatype/old_datatype_data.ML\<close> |
520 ML_file "Tools/Old_Datatype/old_rep_datatype.ML" |
520 ML_file \<open>Tools/Old_Datatype/old_rep_datatype.ML\<close> |
521 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML" |
521 ML_file \<open>Tools/Old_Datatype/old_datatype_codegen.ML\<close> |
522 ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML" |
522 ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_util.ML\<close> |
523 ML_file "Tools/Old_Datatype/old_primrec.ML" |
523 ML_file \<open>Tools/Old_Datatype/old_primrec.ML\<close> |
524 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML" |
524 ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar.ML\<close> |
525 |
525 |
526 text \<open>Lambda-abstractions with pattern matching:\<close> |
526 text \<open>Lambda-abstractions with pattern matching:\<close> |
527 syntax (ASCII) |
527 syntax (ASCII) |
528 "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" ("(%_)" 10) |
528 "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" ("(%_)" 10) |
529 syntax |
529 syntax |