Thu, 25 Oct 2001 20:04:43 +0200 Replaced main proof by proper Isar script.
berghofe [Thu, 25 Oct 2001 20:04:43 +0200] rev 11935
Replaced main proof by proper Isar script.
Thu, 25 Oct 2001 20:00:11 +0200 derived operations are now: make, extend, truncate (cf. derived_defs);
wenzelm [Thu, 25 Oct 2001 20:00:11 +0200] rev 11934
derived operations are now: make, extend, truncate (cf. derived_defs);
Thu, 25 Oct 2001 19:59:00 +0200 tuned;
wenzelm [Thu, 25 Oct 2001 19:59:00 +0200] rev 11933
tuned;
Thu, 25 Oct 2001 19:55:41 +0200 check_goal: setmp proofs 0;
wenzelm [Thu, 25 Oct 2001 19:55:41 +0200] rev 11932
check_goal: setmp proofs 0;
Thu, 25 Oct 2001 16:09:39 +0200 added windowlistener (can now close the frame by window controls)
kleing [Thu, 25 Oct 2001 16:09:39 +0200] rev 11931
added windowlistener (can now close the frame by window controls)
Thu, 25 Oct 2001 02:13:02 +0200 * HOL/record:
wenzelm [Thu, 25 Oct 2001 02:13:02 +0200] rev 11930
* HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - "record" operation truncates to particular fixed record (acts like a type cast); - make_defs no longer part of default simps; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;
Thu, 25 Oct 2001 02:12:10 +0200 innermost_params;
wenzelm [Thu, 25 Oct 2001 02:12:10 +0200] rev 11929
innermost_params;
Thu, 25 Oct 2001 02:11:49 +0200 (simp add: point.make_def);
wenzelm [Thu, 25 Oct 2001 02:11:49 +0200] rev 11928
(simp add: point.make_def);
Thu, 25 Oct 2001 02:11:28 +0200 provodes induct/cases for use with corresponding Isar methods;
wenzelm [Thu, 25 Oct 2001 02:11:28 +0200] rev 11927
provodes induct/cases for use with corresponding Isar methods; "record" operation (acts as type cast); internal field_inducts, field_cases; make_defs no longer declared as simps; fixed printing of fixed records;
Wed, 24 Oct 2001 19:20:02 +0200 further 1.73 changes: added fix_direct, simplified assume interface;
wenzelm [Wed, 24 Oct 2001 19:20:02 +0200] rev 11926
further 1.73 changes: added fix_direct, simplified assume interface;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip