Tue, 01 Jun 2010 13:54:33 +0200 use local /home/isatest/polyml-5.3.0 on atbroy102 to avoid problems with the SMB filesystem via homebroy;
wenzelm [Tue, 01 Jun 2010 13:54:33 +0200] rev 37240
use local /home/isatest/polyml-5.3.0 on atbroy102 to avoid problems with the SMB filesystem via homebroy;
Tue, 01 Jun 2010 13:32:05 +0200 uniform ML environment setup for Isar and PG;
wenzelm [Tue, 01 Jun 2010 13:32:05 +0200] rev 37239
uniform ML environment setup for Isar and PG;
Tue, 01 Jun 2010 12:16:40 +0200 merged
berghofe [Tue, 01 Jun 2010 12:16:40 +0200] rev 37238
merged
Tue, 01 Jun 2010 11:39:51 +0200 Renamed TypeInfer to Type_Infer.
berghofe [Tue, 01 Jun 2010 11:39:51 +0200] rev 37237
Renamed TypeInfer to Type_Infer.
Tue, 01 Jun 2010 11:30:57 +0200 merged
berghofe [Tue, 01 Jun 2010 11:30:57 +0200] rev 37236
merged
Tue, 01 Jun 2010 11:16:16 +0200 assign now applies meet before update_new to avoid misleading error message.
berghofe [Tue, 01 Jun 2010 11:16:16 +0200] rev 37235
assign now applies meet before update_new to avoid misleading error message.
Tue, 01 Jun 2010 11:13:40 +0200 Tuned.
berghofe [Tue, 01 Jun 2010 11:13:40 +0200] rev 37234
Tuned.
Tue, 01 Jun 2010 11:13:09 +0200 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe [Tue, 01 Jun 2010 11:13:09 +0200] rev 37233
Adapted to new format of proof terms containing explicit proofs of class membership.
Tue, 01 Jun 2010 11:04:49 +0200 classrel and arity theorems are now stored under proper name in theory. add_arity and
berghofe [Tue, 01 Jun 2010 11:04:49 +0200] rev 37232
classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored.
Tue, 01 Jun 2010 11:01:16 +0200 - outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe [Tue, 01 Jun 2010 11:01:16 +0200] rev 37231
- outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip