Changes

Summary

tuned;
formal position for PThm nodes;
clarified ML types;
proper treatment of body oracles, outside of recursion into thms graph;

Changeset 70495:aaafff824632 by wenzelm: tuned;
The file was modified	`src/Pure/proofterm.ML` (diff)
Changeset 70494:41108e3e9ca5 by wenzelm: formal position for PThm nodes;
The file was modified	`src/HOL/HOLCF/Tools/cont_proc.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_axiomatization.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_comp.ML` (diff)
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_fp_n2m.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_fp_util.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_gfp.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.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_compat.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.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lfp_size.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_tactics.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML` (diff)
The file was modified	`src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML` (diff)
The file was modified	`src/HOL/Tools/Function/function.ML` (diff)
The file was modified	`src/HOL/Tools/Function/function_core.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_bnf.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def_code_dt.ML` (diff)
The file was modified	`src/HOL/Tools/Meson/meson_clausify.ML` (diff)
The file was modified	`src/HOL/Tools/Transfer/transfer_bnf.ML` (diff)
The file was modified	`src/Pure/General/binding.ML` (diff)
The file was modified	`src/Pure/Isar/code.ML` (diff)
The file was modified	`src/Pure/Isar/element.ML` (diff)
The file was modified	`src/Pure/Isar/generic_target.ML` (diff)
The file was modified	`src/Pure/Isar/proof.ML` (diff)
The file was modified	`src/Pure/Isar/proof_context.ML` (diff)
The file was modified	`src/Pure/ML/ml_thms.ML` (diff)
The file was modified	`src/Pure/Proof/extraction.ML` (diff)
The file was modified	`src/Pure/drule.ML` (diff)
The file was modified	`src/Pure/global_theory.ML` (diff)
The file was modified	`src/Pure/goal.ML` (diff)
The file was modified	`src/Pure/proofterm.ML` (diff)
The file was modified	`src/Pure/thm.ML` (diff)
Changeset 70493:a9053fa30909 by wenzelm: clarified ML types;
The file was modified	`src/HOL/Tools/inductive_realizer.ML` (diff)
The file was modified	`src/HOL/Tools/rewrite_hol_proof.ML` (diff)
The file was modified	`src/Pure/Proof/extraction.ML` (diff)
The file was modified	`src/Pure/Proof/proof_checker.ML` (diff)
The file was modified	`src/Pure/Proof/proof_rewrite_rules.ML` (diff)
The file was modified	`src/Pure/Proof/proof_syntax.ML` (diff)
The file was modified	`src/Pure/proofterm.ML` (diff)
Changeset 70492:c65ccd813f4d by wenzelm: proper treatment of body oracles, outside of recursion into thms graph;
The file was modified	`src/Pure/proofterm.ML` (diff)