5 months ago immler [Thu, 17 Jan 2019 16:28:07 -0500] rev 69681
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
src/HOL/Analysis/Cross3.thy src/HOL/Analysis/Extended_Real_Limits.thy src/HOL/Analysis/Fashoda_Theorem.thy src/HOL/Analysis/Finite_Cartesian_Product.thy src/HOL/Analysis/Finite_Product_Measure.thy src/HOL/Analysis/Function_Topology.thy src/HOL/Analysis/Further_Topology.thy src/HOL/Analysis/Great_Picard.thy src/HOL/Analysis/Homeomorphism.thy src/HOL/Analysis/Improper_Integral.thy src/HOL/Analysis/Interval_Integral.thy src/HOL/Analysis/Tagged_Division.thy

5 months ago immler [Thu, 17 Jan 2019 16:22:21 -0500] rev 69680
revert to 56acd449da41
src/HOL/Analysis/Cross3.thy src/HOL/Analysis/Determinants.thy src/HOL/Analysis/Extended_Real_Limits.thy src/HOL/Analysis/Fashoda_Theorem.thy src/HOL/Analysis/Finite_Cartesian_Product.thy src/HOL/Analysis/Finite_Product_Measure.thy src/HOL/Analysis/Function_Topology.thy src/HOL/Analysis/Further_Topology.thy src/HOL/Analysis/Great_Picard.thy src/HOL/Analysis/Homeomorphism.thy src/HOL/Analysis/Improper_Integral.thy src/HOL/Analysis/Interval_Integral.thy src/HOL/Analysis/Tagged_Division.thy

5 months ago Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk> [Thu, 17 Jan 2019 16:08:41 +0000] rev 69679
merge
src/HOL/Analysis/Cartesian_Space.thy src/HOL/Analysis/Change_Of_Vars.thy src/HOL/Analysis/Cross3.thy src/HOL/Analysis/Determinants.thy

5 months ago Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk> [Thu, 17 Jan 2019 15:50:28 +0000] rev 69678
more tagging
src/HOL/Analysis/Cartesian_Euclidean_Space.thy src/HOL/Analysis/Cartesian_Space.thy src/HOL/Analysis/Finite_Cartesian_Product.thy src/HOL/Analysis/Further_Topology.thy src/HOL/Analysis/Great_Picard.thy src/HOL/Analysis/Homeomorphism.thy src/HOL/Analysis/Improper_Integral.thy src/HOL/Analysis/Interval_Integral.thy src/HOL/Library/Numeral_Type.thy

5 months ago Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk> [Wed, 16 Jan 2019 21:27:33 +0000] rev 69677
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
NEWS src/Doc/System/Sessions.thy src/HOL/Analysis/Cartesian_Euclidean_Space.thy src/HOL/Analysis/Cartesian_Space.thy src/HOL/Analysis/Change_Of_Vars.thy src/HOL/Analysis/Cross3.thy src/HOL/Analysis/Determinants.thy src/HOL/Analysis/Extended_Real_Limits.thy src/HOL/Analysis/Fashoda_Theorem.thy src/HOL/Analysis/Finite_Cartesian_Product.thy src/HOL/Analysis/Finite_Product_Measure.thy src/HOL/Analysis/Function_Topology.thy src/HOL/Analysis/Henstock_Kurzweil_Integration.thy src/HOL/Analysis/Tagged_Division.thy src/HOL/Library/Cardinality.thy src/HOL/Library/Numeral_Type.thy src/Pure/General/path.ML src/Pure/General/path.scala src/Pure/Pure.thy src/Pure/Thy/export.scala src/Pure/Thy/sessions.ML src/Pure/Thy/sessions.scala src/Pure/Tools/build.scala src/Pure/Tools/generated_files.ML src/Tools/Haskell/Haskell.thy src/Tools/Haskell/Test.thy

5 months ago immler [Wed, 16 Jan 2019 19:34:48 -0500] rev 69676
chapters for analysis manual
src/HOL/Analysis/Analysis.thy src/HOL/Analysis/Elementary_Metric_Spaces.thy src/HOL/Analysis/Elementary_Topology.thy src/HOL/Analysis/L2_Norm.thy src/HOL/Analysis/Sigma_Algebra.thy src/HOL/Analysis/Starlike.thy src/HOL/Analysis/Topology_Euclidean_Space.thy src/HOL/Analysis/document/root.tex

5 months ago immler [Wed, 16 Jan 2019 18:14:02 -0500] rev 69675
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
src/HOL/Analysis/Cartesian_Space.thy src/HOL/Analysis/Change_Of_Vars.thy src/HOL/Analysis/Convex.thy src/HOL/Analysis/Cross3.thy src/HOL/Analysis/Determinants.thy src/HOL/Analysis/Linear_Algebra.thy src/HOL/Analysis/Starlike.thy

5 months ago immler [Wed, 16 Jan 2019 16:50:35 -0500] rev 69674
bundle syntax for inner
src/HOL/Analysis/Inner_Product.thy src/HOL/Analysis/Linear_Algebra.thy

5 months ago wenzelm [Wed, 16 Jan 2019 18:54:18 +0100] rev 69673
merged

5 months ago wenzelm [Wed, 16 Jan 2019 17:56:29 +0100] rev 69672
tuned;
NEWS