| Fri, 28 Jul 2006 17:30:20 +0200 |
wneuper |
store_* theory-elements added, inhibit overwriting in Isac.ML does not yet work
start_Take
|
changeset |
files
|
| Thu, 27 Jul 2006 18:54:47 +0200 |
wneuper |
work on error in locate_gen: ([1],Frm)-->([2],Res)
start_Take
|
changeset |
files
|
| Thu, 27 Jul 2006 18:09:17 +0200 |
wneuper |
implemented setContext..Thy;
start_Take
|
changeset |
files
|
| Thu, 27 Jul 2006 13:14:34 +0200 |
wneuper |
bugfix in refineProblem
start_Take
|
changeset |
files
|
| Thu, 27 Jul 2006 12:27:32 +0200 |
wneuper |
on inserting a formula in a calculation cut the tree down to result
start_Take
|
changeset |
files
|
| Thu, 27 Jul 2006 11:12:21 +0200 |
wneuper |
code polishing
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 19:30:02 +0200 |
wneuper |
updated refineProblem
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 19:01:11 +0200 |
wneuper |
debugging setContext; pbl ok
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 16:25:22 +0200 |
wneuper |
sml: prepare rewriter to return the position of thm-application
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 16:14:15 +0200 |
wneuper |
sml: repair on checkContext
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 14:53:28 +0200 |
wneuper |
sml: added setContext; missing for theories
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 14:16:47 +0200 |
wneuper |
sml: improved initContext Thy_
start_Take
|
changeset |
files
|
| Wed, 26 Jul 2006 10:32:38 +0200 |
wneuper |
sml: XML-details corrected
start_Take
|
changeset |
files
|
| Tue, 25 Jul 2006 13:21:39 +0200 |
wneuper |
sml: made context-handling more robust
start_Take
|
changeset |
files
|
| Tue, 25 Jul 2006 12:36:39 +0200 |
wneuper |
sml: xml-format polished
start_Take
|
changeset |
files
|
| Mon, 24 Jul 2006 19:58:36 +0200 |
wneuper |
preparing for rewriter returning location of applying a Thm or Calc;
start_Take
|
changeset |
files
|
| Mon, 24 Jul 2006 17:16:59 +0200 |
wneuper |
preparing for rewriter returning location of applying a Thm or Calc
start_Take
|
changeset |
files
|
| Mon, 24 Jul 2006 15:44:09 +0200 |
wneuper |
sml: repair for mets2file
start_Take
|
changeset |
files
|
| Mon, 24 Jul 2006 15:36:50 +0200 |
wneuper |
finished context for pbl met
start_Take
|
changeset |
files
|
| Fri, 21 Jul 2006 16:43:38 +0200 |
wneuper |
sml: adapted checkContext to signature agreed upon
start_Take
|
changeset |
files
|
| Fri, 21 Jul 2006 15:56:52 +0200 |
wneuper |
sml: added guh2kestoreID for checkContext
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 20:28:17 +0200 |
wneuper |
prepare for running 'pbls2file' with references
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 19:41:07 +0200 |
wneuper |
prepare for running 'pbls2file' with references
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 16:50:53 +0200 |
wneuper |
sml: 'type met' added {guh, authors, ...} finished
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 16:25:58 +0200 |
wneuper |
sml: 'type met' added {guh, authors, ...}, missing: check_guh_unique
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 16:09:41 +0200 |
wneuper |
sml: 'type met' added {guh, authors, ...}, missing: check_guh_unique, tests
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 14:01:48 +0200 |
wneuper |
sml: 'type pbt' added {guh, authors, ...}, check_guh_unique, tests done
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 11:28:43 +0200 |
wneuper |
added 'fun kestoreID2guh' for keref2xml, impl. missing
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 10:54:50 +0200 |
wneuper |
sml: 'type pbt' added {guh, authors, ...}, missing: check_guh_unique, tests
start_Take
|
changeset |
files
|
| Thu, 20 Jul 2006 09:45:34 +0200 |
wneuper |
sml: prepare for 'type pbt' adding {guh, authors, ...}
start_Take
|
changeset |
files
|
| Wed, 19 Jul 2006 19:36:19 +0200 |
wneuper |
sml: guh2theID tested with checkContext Thy_
start_Take
|
changeset |
files
|
| Wed, 19 Jul 2006 18:22:30 +0200 |
wneuper |
sml: added guh2theID
start_Take
|
changeset |
files
|
| Wed, 19 Jul 2006 16:49:06 +0200 |
wneuper |
cleared doubled code on 'fun subst2str''
start_Take
|
changeset |
files
|
| Wed, 19 Jul 2006 15:53:33 +0200 |
wneuper |
sml: finished 'fun conttyh2xml'
start_Take
|
changeset |
files
|
| Wed, 19 Jul 2006 15:20:21 +0200 |
wneuper |
included thy into 'type contthy' for *2guh
start_Take
|
changeset |
files
|
| Tue, 18 Jul 2006 18:38:11 +0200 |
wneuper |
sml: work on 'fun context_thy', Notappl added
start_Take
|
changeset |
files
|
| Tue, 18 Jul 2006 17:20:46 +0200 |
wneuper |
sml: work on 'fun context_thy', Notappl missing
start_Take
|
changeset |
files
|
| 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
|