Fri, 01 Jul 2005 14:42:00 +0200 ctyp: added 'sorts' field;
wenzelm [Fri, 01 Jul 2005 14:42:00 +0200] rev 16656
ctyp: added 'sorts' field; may_insert_typ/term/env_sorts: observe Sign.all_sorts_nonempty; may_insert_env_sorts: insert sorts of type subst only; instantiate: insert sorts of insts; tuned;
Fri, 01 Jul 2005 14:41:59 +0200 added all_sorts_nonempty;
wenzelm [Fri, 01 Jul 2005 14:41:59 +0200] rev 16655
added all_sorts_nonempty;
Fri, 01 Jul 2005 14:41:58 +0200 low-level tuning of fold, fold_rev, foldl_map;
wenzelm [Fri, 01 Jul 2005 14:41:58 +0200] rev 16654
low-level tuning of fold, fold_rev, foldl_map;
Fri, 01 Jul 2005 14:41:57 +0200 isatool install: removed KDE option;
wenzelm [Fri, 01 Jul 2005 14:41:57 +0200] rev 16653
isatool install: removed KDE option;
Fri, 01 Jul 2005 14:22:33 +0200 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe [Fri, 01 Jul 2005 14:22:33 +0200] rev 16652
Fixed bug: lookup' must use = instead of eq_type to compare types of variables, otherwise pattern matching algorithm may loop.
Fri, 01 Jul 2005 14:20:01 +0200 Changed interface of Envir.lookup'
berghofe [Fri, 01 Jul 2005 14:20:01 +0200] rev 16651
Changed interface of Envir.lookup'
Fri, 01 Jul 2005 14:19:36 +0200 Moved eq_type from envir.ML to type.ML
berghofe [Fri, 01 Jul 2005 14:19:36 +0200] rev 16650
Moved eq_type from envir.ML to type.ML
Fri, 01 Jul 2005 14:18:27 +0200 Implemented modular code generation.
berghofe [Fri, 01 Jul 2005 14:18:27 +0200] rev 16649
Implemented modular code generation.
Fri, 01 Jul 2005 14:17:32 +0200 Simplified proof (thanks to strengthened ball_cong).
berghofe [Fri, 01 Jul 2005 14:17:32 +0200] rev 16648
Simplified proof (thanks to strengthened ball_cong).
Fri, 01 Jul 2005 14:16:32 +0200 Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
berghofe [Fri, 01 Jul 2005 14:16:32 +0200] rev 16647
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip