Changes

Summary

proper concept of code declaration wrt. atomicity and Isar declarations

Changeset 66251:cd935b7cb3fb by haftmann: proper concept of code declaration wrt. atomicity and Isar declarations
The file was modified	`src/Doc/Codegen/Further.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Candidates.thy` (diff)
The file was modified	`src/HOL/Codegenerator_Test/Generate.thy` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/Library/Mapping.thy` (diff)
The file was modified	`src/HOL/Library/old_recdef.ML` (diff)
The file was modified	`src/HOL/Predicate.thy` (diff)
The file was modified	`src/HOL/Product_Type.thy` (diff)
The file was modified	`src/HOL/String.thy` (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_grec_sugar.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_compat.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/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/Function/function.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_setup.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_primrec.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_rep_datatype.ML` (diff)
The file was modified	`src/HOL/Tools/Old_Datatype/old_size.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML` (diff)
The file was modified	`src/HOL/Tools/Quickcheck/narrowing_generators.ML` (diff)
The file was modified	`src/HOL/Tools/Quickcheck/quickcheck_common.ML` (diff)
The file was modified	`src/HOL/Tools/Quickcheck/random_generators.ML` (diff)
The file was modified	`src/HOL/Tools/code_evaluation.ML` (diff)
The file was modified	`src/HOL/Tools/record.ML` (diff)
The file was modified	`src/Pure/Isar/code.ML` (diff)
The file was modified	`src/Pure/Isar/specification.ML` (diff)
The file was modified	`src/Pure/Proof/extraction.ML` (diff)
The file was modified	`src/Pure/Pure.thy` (diff)