| Thu, 17 Jan 2008 16:27:03 +0100 |
start-work-070517 merged into HEAD
|
file | diff | annotate |
| Thu, 22 Feb 2007 16:26:13 +0100 |
merged in start_Take (smltest/xmlsrc required manual copy)
|
file | diff | annotate |
| Wed, 30 Aug 2006 18:50:46 +0200 |
preparing SK: improved getTactic for "sym_..."
|
file | diff | annotate |
| Wed, 30 Aug 2006 12:16:45 +0200 |
preparing SK: improved reverse rewrite cancel_p
|
file | diff | annotate |
| Tue, 29 Aug 2006 13:30:35 +0200 |
preparing SK: improve reverse rewrite cancel_p, intermediate state
|
file | diff | annotate |
| Tue, 29 Aug 2006 11:43:53 +0200 |
preparing SK: improve reverse rewrite cancel_p, intermediate state
|
file | diff | annotate |
| Tue, 29 Aug 2006 10:07:24 +0200 |
preparing SK: improve reverse rewrite cancel_p, intermediate state
|
file | diff | annotate |
| Fri, 25 Aug 2006 16:46:20 +0200 |
repair reverse rewrite; has been broken by extending 'type rule' with 'Rls_'
|
file | diff | annotate |
| Fri, 28 Jul 2006 17:30:20 +0200 |
store_* theory-elements added, inhibit overwriting in Isac.ML does not yet work
|
file | diff | annotate |
| Wed, 26 Jul 2006 16:14:15 +0200 |
sml: repair on checkContext
|
file | diff | annotate |
| Wed, 26 Jul 2006 10:32:38 +0200 |
sml: XML-details corrected
|
file | diff | annotate |
| Tue, 25 Jul 2006 13:21:39 +0200 |
sml: made context-handling more robust
|
file | diff | annotate |
| Mon, 24 Jul 2006 19:58:36 +0200 |
preparing for rewriter returning location of applying a Thm or Calc;
|
file | diff | annotate |
| Fri, 21 Jul 2006 15:56:52 +0200 |
sml: added guh2kestoreID for checkContext
|
file | diff | annotate |
| Thu, 20 Jul 2006 19:41:07 +0200 |
prepare for running 'pbls2file' with references
|
file | diff | annotate |
| Thu, 20 Jul 2006 14:01:48 +0200 |
sml: 'type pbt' added {guh, authors, ...}, check_guh_unique, tests done
|
file | diff | annotate |
| Thu, 20 Jul 2006 11:28:43 +0200 |
added 'fun kestoreID2guh' for keref2xml, impl. missing
|
file | diff | annotate |
| Wed, 19 Jul 2006 18:22:30 +0200 |
sml: added guh2theID
|
file | diff | annotate |
| Wed, 19 Jul 2006 15:20:21 +0200 |
included thy into 'type contthy' for *2guh
|
file | diff | annotate |
| Tue, 18 Jul 2006 18:38:11 +0200 |
sml: work on 'fun context_thy', Notappl added
|
file | diff | annotate |
| Tue, 18 Jul 2006 17:20:46 +0200 |
sml: work on 'fun context_thy', Notappl missing
|
file | diff | annotate |
| Mon, 17 Jul 2006 10:17:33 +0200 |
sml: thydata2xml goes through
|
file | diff | annotate |
| Fri, 14 Jul 2006 18:20:42 +0200 |
sml: thydata2xml goes until Poly.thy
|
file | diff | annotate |
| Fri, 14 Jul 2006 15:38:15 +0200 |
sml: thy_hierarchy is ok
|
file | diff | annotate |
| Fri, 14 Jul 2006 10:44:50 +0200 |
sml: thydata2xml includes rls, rules (excl. Calc),
|
file | diff | annotate |
| Thu, 13 Jul 2006 16:50:54 +0200 |
made guh <1--1> theID
|
file | diff | annotate |
| Wed, 12 Jul 2006 17:58:31 +0200 |
sml: thy_hierarchy now contains Isabelle's theorems used in isac's rls's
|
file | diff | annotate |
| Wed, 12 Jul 2006 13:47:49 +0200 |
'fun thydata2xml': theory elements to xml finished;
|
file | diff | annotate |
| Fri, 07 Jul 2006 16:50:35 +0200 |
finished thy_containing_rls for contthy
|
file | diff | annotate |
| Thu, 06 Jul 2006 17:22:19 +0200 |
work on 'fun rls2xml', intermediate
|
file | diff | annotate |
| Mon, 26 Jun 2006 17:15:56 +0200 |
extended 'type thydata' with guh and authors
|
file | diff | annotate |
| Mon, 26 Jun 2006 16:27:56 +0200 |
finished thy_hierarchy
|
file | diff | annotate |
| Wed, 21 Jun 2006 15:46:15 +0200 |
sml: work on thy-hierarchy, intermediate;
|
file | diff | annotate |
| Sat, 17 Jun 2006 15:38:27 +0200 |
sml: matchTheory and getContextToThy, tested ok
|
file | diff | annotate |
| Sat, 17 Jun 2006 06:39:58 +0200 |
sml: matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Fri, 16 Jun 2006 13:58:28 +0200 |
sml: matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Fri, 16 Jun 2006 11:35:23 +0200 |
sml: matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Fri, 16 Jun 2006 09:13:26 +0200 |
sml: matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Sun, 11 Jun 2006 12:38:55 +0200 |
matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Sun, 11 Jun 2006 11:57:48 +0200 |
mv systest/ctree.sml ../smltest/ME/ctree.sml;
|
file | diff | annotate |
| Sun, 11 Jun 2006 10:41:16 +0200 |
matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Sun, 11 Jun 2006 07:18:01 +0200 |
matchTheory and getContextToThy, intermediately
|
file | diff | annotate |
| Sat, 10 Jun 2006 10:15:07 +0200 |
introduced 'type rew_ord' for 'type contthy'
|
file | diff | annotate |
| Sat, 10 Jun 2006 09:20:03 +0200 |
mv ME/reverse-rew.sml ME/rewtools.sml for getContextToThy
|
file | diff | annotate |
| Fri, 04 Jan 2008 16:08:52 +0100 |
for PolyMinus at Sch"arding, make p.33 confluent
|
file | diff | annotate |
| Fri, 04 Jan 2008 11:16:28 +0100 |
for PolyMinus at Sch"arding, make p.33 confluent
|
file | diff | annotate |
| Wed, 02 Jan 2008 18:13:59 +0100 |
sel_rules + sel_appl_atomic_tacs + applyTactic, intermediate state
|
file | diff | annotate |
| Wed, 02 Jan 2008 14:42:04 +0100 |
sel_rules: generalize "fun assod" to Rewrite tac -- Rewrite_Set containing tac, stopped withou success.
|
file | diff | annotate |
| Wed, 02 Jan 2008 09:56:26 +0100 |
sel_rules: generalize "fun assod" to Rewrite tac -- Rewrite_Set containing tac, intermediate
|
file | diff | annotate |
| Mon, 31 Dec 2007 17:56:24 +0100 |
sel_rules: sel_appl_atomic_tacs finished
|
file | diff | annotate |
| Mon, 31 Dec 2007 14:18:53 +0100 |
sel_rules selects _applicable_ tactics only, intermediate stae
|
file | diff | annotate |
| Mon, 31 Dec 2007 09:55:43 +0100 |
for PolyMinus at Sch"arding, p.34 finshed
|
file | diff | annotate |