2013-04-25 hoelzl [Thu, 25 Apr 2013 11:59:21 +0200] rev 51775
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
NEWS src/HOL/Conditionally_Complete_Lattices.thy src/HOL/Library/Extended_Real.thy src/HOL/Real.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Topological_Spaces.thy

2013-04-25 hoelzl [Thu, 25 Apr 2013 10:35:56 +0200] rev 51774
renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
NEWS src/HOL/Conditionally_Complete_Lattices.thy src/HOL/Library/Extended_Real.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Topological_Spaces.thy

2013-04-24 hoelzl [Wed, 24 Apr 2013 13:28:30 +0200] rev 51773
spell conditional_ly_-complete lattices correct
NEWS src/HOL/Conditional_Complete_Lattices.thy src/HOL/Conditionally_Complete_Lattices.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Real.thy src/HOL/Topological_Spaces.thy

2013-04-25 traytel [Thu, 25 Apr 2013 10:31:10 +0200] rev 51772
specify nicer names for map, set and rel in the stream library
src/HOL/BNF/Examples/Koenig.thy src/HOL/BNF/Examples/Stream.thy

2013-04-25 blanchet [Thu, 25 Apr 2013 09:25:50 +0200] rev 51771
start making "wrap_data" more robust
src/HOL/BNF/Tools/bnf_wrap.ML

2013-04-25 blanchet [Thu, 25 Apr 2013 08:56:37 +0200] rev 51770
no eta-expansion for case in split rules and case_conv
src/HOL/BNF/Tools/bnf_wrap.ML

2013-04-25 blanchet [Thu, 25 Apr 2013 08:56:10 +0200] rev 51769
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 22:48:22 +0200] rev 51768
proper error generated for wrong mixfix
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 18:49:52 +0200] rev 51767
honor user-specified name for relator + generalize syntax
src/HOL/BNF/Tools/bnf_comp.ML src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_fp.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_util.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 17:47:22 +0200] rev 51766
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
src/HOL/BNF/Examples/Stream.thy src/HOL/BNF/Examples/TreeFI.thy src/HOL/BNF/More_BNFs.thy src/HOL/BNF/Tools/bnf_comp.ML src/HOL/BNF/Tools/bnf_comp_tactics.ML src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_def_tactics.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_gfp_tactics.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_lfp_tactics.ML