Changes

Summary

added command 'export_generated_files'; clarified signature;
tuned proofs
canonical operation to typeset generated code makes dedicated environment obsolete
tuned
tuned language

Changeset 69662:fd86ed39aea4 by wenzelm: added command 'export_generated_files';<br>clarified signature;
The file was modified	`src/Pure/Pure.thy` (diff)
The file was modified	`src/Pure/Tools/generated_files.ML` (diff)
The file was modified	`src/Tools/Haskell/Haskell.thy` (diff)
The file was modified	`src/Tools/Haskell/Test.thy` (diff)
Changeset 69661:a03a63b81f44 by haftmann: tuned proofs
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Brouwer_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Analysis/Caratheodory.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Normed_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Extended_Real_Limits.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Homeomorphism.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Regularity.thy` (diff)
The file was modified	`src/HOL/Analysis/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
The file was modified	`src/HOL/Analysis/Winding_Numbers.thy` (diff)
The file was modified	`src/HOL/Cardinals/Ordinal_Arithmetic.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellorder_Constructions.thy` (diff)
The file was modified	`src/HOL/Fun.thy` (diff)
The file was modified	`src/HOL/HOLCF/Universal.thy` (diff)
The file was modified	`src/HOL/IMP/Denotational.thy` (diff)
The file was modified	`src/HOL/Library/AList.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/Infinite_Set.thy` (diff)
The file was modified	`src/HOL/Library/Liminf_Limsup.thy` (diff)
The file was modified	`src/HOL/Library/Multiset_Permutations.thy` (diff)
The file was modified	`src/HOL/Library/Numeral_Type.thy` (diff)
The file was modified	`src/HOL/Library/Option_ord.thy` (diff)
The file was modified	`src/HOL/Library/Order_Continuity.thy` (diff)
The file was modified	`src/HOL/Library/Ramsey.thy` (diff)
The file was modified	`src/HOL/MicroJava/Comp/LemmasComp.thy` (diff)
The file was modified	`src/HOL/Nat.thy` (diff)
The file was modified	`src/HOL/Probability/Fin_Map.thy` (diff)
The file was modified	`src/HOL/Probability/Information.thy` (diff)
The file was modified	`src/HOL/Probability/SPMF.thy` (diff)
The file was modified	`src/HOL/Rings.thy` (diff)
The file was modified	`src/HOL/UNITY/FP.thy` (diff)
The file was modified	`src/HOL/UNITY/Transformers.thy` (diff)
The file was modified	`src/HOL/ZF/Zet.thy` (diff)
Changeset 69660:2bc2a8599369 by haftmann: canonical operation to typeset generated code makes dedicated environment obsolete
The file was modified	`src/Doc/Classes/Classes.thy` (diff)
The file was modified	`src/Doc/Classes/document/style.sty` (diff)
The file was modified	`src/Doc/Codegen/Adaptation.thy` (diff)
The file was modified	`src/Doc/Codegen/Computations.thy` (diff)
The file was modified	`src/Doc/Codegen/Foundations.thy` (diff)
The file was modified	`src/Doc/Codegen/Further.thy` (diff)
The file was modified	`src/Doc/Codegen/Introduction.thy` (diff)
The file was modified	`src/Doc/Codegen/Refinement.thy` (diff)
The file was modified	`src/Doc/Codegen/document/style.sty` (diff)
The file was modified	`src/Tools/Code/code_target.ML` (diff)
Changeset 69659:07025152dd80 by haftmann: tuned
The file was modified	`src/Tools/Code/code_printer.ML` (diff)
Changeset 69658:7357a4f79f60 by haftmann: tuned language
The file was modified	`src/Doc/Codegen/Evaluation.thy` (diff)