Changes

Summary

clarified session; tuned headers;
tuned header;
simplified -- always produce heap for RAW, Pure;

Changeset 62479:716336f19aa9 by wenzelm: clarified session;<br>tuned headers;
The file was added	`src/HOL/Nonstandard_Analysis/CLim.thy`
The file was added	`src/HOL/Nonstandard_Analysis/CStar.thy`
The file was added	`src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy`
The file was added	`src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HDeriv.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HLim.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HLog.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HSEQ.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HSeries.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HTranscendental.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HyperDef.thy`
The file was added	`src/HOL/Nonstandard_Analysis/HyperNat.thy`
The file was added	`src/HOL/Nonstandard_Analysis/Hypercomplex.thy`
The file was added	`src/HOL/Nonstandard_Analysis/Hyperreal.thy`
The file was added	`src/HOL/Nonstandard_Analysis/NSA.thy`
The file was added	`src/HOL/Nonstandard_Analysis/NSCA.thy`
The file was added	`src/HOL/Nonstandard_Analysis/NSComplex.thy`
The file was added	`src/HOL/Nonstandard_Analysis/NatStar.thy`
The file was added	`src/HOL/Nonstandard_Analysis/Star.thy`
The file was added	`src/HOL/Nonstandard_Analysis/StarDef.thy`
The file was added	`src/HOL/Nonstandard_Analysis/document/root.tex`
The file was added	`src/HOL/Nonstandard_Analysis/transfer.ML`
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/ROOT` (diff)
The file was removed	`src/HOL/NSA/CLim.thy`
The file was removed	`src/HOL/NSA/CStar.thy`
The file was removed	`src/HOL/NSA/Examples/NSPrimes.thy`
The file was removed	`src/HOL/NSA/Free_Ultrafilter.thy`
The file was removed	`src/HOL/NSA/HDeriv.thy`
The file was removed	`src/HOL/NSA/HLim.thy`
The file was removed	`src/HOL/NSA/HLog.thy`
The file was removed	`src/HOL/NSA/HSEQ.thy`
The file was removed	`src/HOL/NSA/HSeries.thy`
The file was removed	`src/HOL/NSA/HTranscendental.thy`
The file was removed	`src/HOL/NSA/HyperDef.thy`
The file was removed	`src/HOL/NSA/HyperNat.thy`
The file was removed	`src/HOL/NSA/Hypercomplex.thy`
The file was removed	`src/HOL/NSA/Hyperreal.thy`
The file was removed	`src/HOL/NSA/NSA.thy`
The file was removed	`src/HOL/NSA/NSCA.thy`
The file was removed	`src/HOL/NSA/NSComplex.thy`
The file was removed	`src/HOL/NSA/NatStar.thy`
The file was removed	`src/HOL/NSA/Star.thy`
The file was removed	`src/HOL/NSA/StarDef.thy`
The file was removed	`src/HOL/NSA/document/root.tex`
The file was removed	`src/HOL/NSA/transfer.ML`
Changeset 62478:a62c86d25024 by wenzelm: tuned header;
The file was modified	`src/Pure/RAW/ml_heap_polyml-5.3.0.ML` (diff)
Changeset 62477:bc6e771e98a6 by wenzelm: simplified -- always produce heap for RAW, Pure;
The file was modified	`src/Pure/Tools/build.scala` (diff)
The file was removed	`src/Pure/build`