| Mon, 17 Jul 2006 20:11:48 +0200 |
wneuper |
sml: repaired tests (norm_Rational of !RG! has been used) after thydata2xml goes through
start_Take
|
changeset |
files
|
| Mon, 17 Jul 2006 10:17:33 +0200 |
wneuper |
sml: thydata2xml goes through
start_Take
|
changeset |
files
|
| Fri, 14 Jul 2006 18:20:42 +0200 |
wneuper |
sml: thydata2xml goes until Poly.thy
start_Take
|
changeset |
files
|
| Fri, 14 Jul 2006 15:38:15 +0200 |
wneuper |
sml: thy_hierarchy is ok
start_Take
|
changeset |
files
|
| Fri, 14 Jul 2006 11:23:23 +0200 |
wneuper |
sml: thydata2xml with RULESETDATA format checked
start_Take
|
changeset |
files
|
| Fri, 14 Jul 2006 10:44:50 +0200 |
wneuper |
sml: thydata2xml includes rls, rules (excl. Calc),
start_Take
|
changeset |
files
|
| Thu, 13 Jul 2006 16:50:54 +0200 |
wneuper |
made guh <1--1> theID
start_Take
|
changeset |
files
|
| Thu, 13 Jul 2006 10:18:34 +0200 |
wneuper |
sml: thy_hierarchy: guh <1--1> theID is broken
start_Take
|
changeset |
files
|
| Wed, 12 Jul 2006 17:58:31 +0200 |
wneuper |
sml: thy_hierarchy now contains Isabelle's theorems used in isac's rls's
start_Take
|
changeset |
files
|
| Wed, 12 Jul 2006 14:09:35 +0200 |
wneuper |
marked old version 'fun calc2xml' for pbl-met-hierarchy to be aligned with thy_hierarchy
start_Take
|
changeset |
files
|
| Wed, 12 Jul 2006 13:47:49 +0200 |
wneuper |
'fun thydata2xml': theory elements to xml finished;
start_Take
|
changeset |
files
|
| Tue, 11 Jul 2006 17:14:08 +0200 |
wneuper |
sml: get_the ["IsacKnowledge"] shows wrong content
start_Take
|
changeset |
files
|
| Tue, 11 Jul 2006 16:46:43 +0200 |
wneuper |
sml: thy_hierarchy ok WITH guhs, going to 'fun thydata2xml'
start_Take
|
changeset |
files
|
| Tue, 11 Jul 2006 14:50:08 +0200 |
wneuper |
sml: thy_hierarchy ok, going to 'fun thydata2xml'
start_Take
|
changeset |
files
|
| Tue, 11 Jul 2006 09:48:31 +0200 |
wneuper |
sml: work on thy_hierarchy
start_Take
|
changeset |
files
|
| Mon, 10 Jul 2006 18:10:39 +0200 |
wneuper |
renamed *Context according to java
start_Take
|
changeset |
files
|
| Fri, 07 Jul 2006 17:20:04 +0200 |
wneuper |
removed a flaw in testsetup
start_Take
|
changeset |
files
|
| Fri, 07 Jul 2006 16:50:35 +0200 |
wneuper |
finished thy_containing_rls for contthy
start_Take
|
changeset |
files
|
| Thu, 06 Jul 2006 17:22:19 +0200 |
wneuper |
work on 'fun rls2xml', intermediate
start_Take
|
changeset |
files
|
| Thu, 29 Jun 2006 18:08:17 +0200 |
wneuper |
work on 'fun rls2xml', intermediate
start_Take
|
changeset |
files
|
| Wed, 28 Jun 2006 10:24:01 +0200 |
wneuper |
added 'fun rules2xml' for 'fun thy_hierarchy'
start_Take
|
changeset |
files
|
| Mon, 26 Jun 2006 17:15:56 +0200 |
wneuper |
extended 'type thydata' with guh and authors
start_Take
|
changeset |
files
|
| Mon, 26 Jun 2006 16:27:56 +0200 |
wneuper |
finished thy_hierarchy
start_Take
|
changeset |
files
|
| Wed, 21 Jun 2006 15:46:15 +0200 |
wneuper |
sml: work on thy-hierarchy, intermediate;
start_Take
|
changeset |
files
|
| Sat, 17 Jun 2006 15:38:27 +0200 |
wneuper |
sml: matchTheory and getContextToThy, tested ok
start_Take
|
changeset |
files
|
| Sat, 17 Jun 2006 06:39:58 +0200 |
wneuper |
sml: matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Fri, 16 Jun 2006 13:58:28 +0200 |
wneuper |
sml: matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Fri, 16 Jun 2006 11:35:23 +0200 |
wneuper |
sml: matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Fri, 16 Jun 2006 09:13:26 +0200 |
wneuper |
sml: matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Sun, 11 Jun 2006 12:38:55 +0200 |
wneuper |
matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Sun, 11 Jun 2006 11:57:48 +0200 |
wneuper |
mv systest/ctree.sml ../smltest/ME/ctree.sml;
start_Take
|
changeset |
files
|
| Sun, 11 Jun 2006 10:41:16 +0200 |
wneuper |
matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Sun, 11 Jun 2006 07:18:01 +0200 |
wneuper |
matchTheory and getContextToThy, intermediately
start_Take
|
changeset |
files
|
| Sat, 10 Jun 2006 10:15:07 +0200 |
wneuper |
introduced 'type rew_ord' for 'type contthy'
start_Take
|
changeset |
files
|
| Sat, 10 Jun 2006 09:20:03 +0200 |
wneuper |
mv ME/reverse-rew.sml ME/rewtools.sml for getContextToThy
start_Take
|
changeset |
files
|
| Fri, 09 Jun 2006 14:01:38 +0200 |
wneuper |
removed a minor bug in 'fun detailstep'
start_Take
|
changeset |
files
|
| Wed, 07 Jun 2006 18:51:07 +0200 |
wneuper |
improved interSteps for Rewrite_Set_Inst;
start_Take
|
changeset |
files
|
| Wed, 07 Jun 2006 17:50:06 +0200 |
wneuper |
removed bug in 'fun init_istate' in generate.sml (which had no effect)
start_Take
|
changeset |
files
|
| Tue, 06 Jun 2006 15:22:15 +0200 |
wneuper |
prepared a test for impl. interSteps for Rewrite_Set_Inst
start_Take
|
changeset |
files
|
| Tue, 06 Jun 2006 13:55:06 +0200 |
wneuper |
work on rule-set's auto-generated scripts for interSteps;
start_Take
|
changeset |
files
|
| Tue, 06 Jun 2006 13:26:49 +0200 |
wneuper |
work on rule-set's auto-generated scripts for interSteps;
start_Take
|
changeset |
files
|
| Tue, 06 Jun 2006 12:04:11 +0200 |
wneuper |
work on rule-set's auto-generated scripts for interSteps;
start_Take
|
changeset |
files
|
| Mon, 05 Jun 2006 17:39:08 +0200 |
wneuper |
work on rule-set's auto-generated scripts for interSteps;
start_Take
|
changeset |
files
|
| Fri, 02 Jun 2006 18:20:21 +0200 |
wneuper |
for interSteps added to ruleset' and corrected fun lev_pred'
start_Take
|
changeset |
files
|
| Sun, 14 May 2006 15:08:28 +0200 |
wneuper |
made getTactic 'Substitute ..' work (quick and dirty: (ab)used STRINGLISTTACTIC for a list of formulae)
start_Take
|
changeset |
files
|
| Sun, 14 May 2006 14:53:45 +0200 |
wneuper |
made getTactic return 'Take cterm', too
start_Take
|
changeset |
files
|
| Sun, 14 May 2006 14:33:20 +0200 |
wneuper |
completed 'fun tac2xml' with 'Substitute cterms'; started and postponed work on reverse rewriting;
start_Take
|
changeset |
files
|
| Sat, 13 May 2006 11:04:20 +0200 |
wneuper |
added: fun tac2xml (Calculate opstr); continued with a flaw introduced with cterm2xml (which (sometimes?) is abused for 'string' in SIMPLETACTIC (and others?))
start_Take
|
changeset |
files
|
| Wed, 10 May 2006 19:34:48 +0200 |
wneuper |
make interSteps run with norm_Rational
start_Take
|
changeset |
files
|
| Wed, 10 May 2006 17:56:10 +0200 |
wneuper |
add calls for prep_rls; introduce coding standard for such calls (not yet followed with all calls!)
start_Take
|
changeset |
files
|
| Wed, 10 May 2006 17:24:51 +0200 |
wneuper |
make interSteps run with norm_Rational
start_Take
|
changeset |
files
|
| Mon, 08 May 2006 17:06:31 +0200 |
wneuper |
mv systest/details.sml ../smltest/ME/solve.sml
start_Take
|
changeset |
files
|
| Mon, 24 Apr 2006 18:19:36 +0200 |
wneuper |
appendFormula and replaceFormula accept formula with syntax error.
start_Take
|
changeset |
files
|
| Fri, 21 Apr 2006 12:45:22 +0200 |
wneuper |
edit comments during implementation of exp in xml: root-equ, systems, calculus
start_Take
|
changeset |
files
|
| Thu, 20 Apr 2006 18:24:18 +0200 |
wneuper |
numbers according to exp_* (done only partially), smltest ok.
start_Take
|
changeset |
files
|
| Wed, 29 Mar 2006 19:13:41 +0200 |
wneuper |
added exp > Rational Simplification
start_Take
|
changeset |
files
|
| Sat, 11 Mar 2006 17:51:13 +0100 |
wneuper |
encode and decode "^^^"<--->"^" at the kernels interface,
start_Take
|
changeset |
files
|
| Sat, 11 Mar 2006 13:39:04 +0100 |
wneuper |
added f2str in some tests (while checking before transfer to exp_)
start_Take
|
changeset |
files
|
| Sat, 25 Feb 2006 17:09:43 +0100 |
wneuper |
replaceFormula CAS-command, finished
start_Take
|
changeset |
files
|
| Sat, 25 Feb 2006 15:41:59 +0100 |
wneuper |
replaceFormula CAS-command, intermediate
start_Take
|
changeset |
files
|