Sat, 27 Mar 2010 15:47:57 +0100 added Term.fold_atyps_sorts convenience;
wenzelm [Sat, 27 Mar 2010 15:47:57 +0100] rev 35986
added Term.fold_atyps_sorts convenience;
Sat, 27 Mar 2010 15:20:31 +0100 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm [Sat, 27 Mar 2010 15:20:31 +0100] rev 35985
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
Sat, 27 Mar 2010 14:10:37 +0100 eliminated old-style Theory.add_defs_i;
wenzelm [Sat, 27 Mar 2010 14:10:37 +0100] rev 35984
eliminated old-style Theory.add_defs_i;
Sat, 27 Mar 2010 02:10:00 +0100 slightly more general simproc (avoids errors of linarith)
boehmes [Sat, 27 Mar 2010 02:10:00 +0100] rev 35983
slightly more general simproc (avoids errors of linarith)
Sat, 27 Mar 2010 00:08:39 +0100 merged
boehmes [Sat, 27 Mar 2010 00:08:39 +0100] rev 35982
merged
Fri, 26 Mar 2010 23:58:27 +0100 updated SMT certificates
boehmes [Fri, 26 Mar 2010 23:58:27 +0100] rev 35981
updated SMT certificates
Fri, 26 Mar 2010 23:57:35 +0100 made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
boehmes [Fri, 26 Mar 2010 23:57:35 +0100] rev 35980
made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
Fri, 26 Mar 2010 23:46:22 +0100 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes [Fri, 26 Mar 2010 23:46:22 +0100] rev 35979
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
Fri, 26 Mar 2010 20:30:03 +0100 merged
wenzelm [Fri, 26 Mar 2010 20:30:03 +0100] rev 35978
merged
Fri, 26 Mar 2010 18:03:01 +0100 Added finite measure space.
hoelzl [Fri, 26 Mar 2010 18:03:01 +0100] rev 35977
Added finite measure space.
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip