Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 27 Mar 2010 14:48:46 +0100] rev 35990
Automated lifting can be restricted to specific quotient types
wenzelm [Sat, 27 Mar 2010 18:07:21 +0100] rev 35989
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
wenzelm [Sat, 27 Mar 2010 17:36:32 +0100] rev 35988
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
eliminated obsolete Sign.cert_def;
misc tuning and clarification;
wenzelm [Sat, 27 Mar 2010 16:01:45 +0100] rev 35987
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm [Sat, 27 Mar 2010 15:47:57 +0100] rev 35986
added Term.fold_atyps_sorts convenience;
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;
wenzelm [Sat, 27 Mar 2010 14:10:37 +0100] rev 35984
eliminated old-style Theory.add_defs_i;
boehmes [Sat, 27 Mar 2010 02:10:00 +0100] rev 35983
slightly more general simproc (avoids errors of linarith)
boehmes [Sat, 27 Mar 2010 00:08:39 +0100] rev 35982
merged
boehmes [Fri, 26 Mar 2010 23:58:27 +0100] rev 35981
updated SMT certificates
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)
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
wenzelm [Fri, 26 Mar 2010 20:30:03 +0100] rev 35978
merged
hoelzl [Fri, 26 Mar 2010 18:03:01 +0100] rev 35977
Added finite measure space.