| Thu, 23 Jan 2020 10:48:57 +0100 |
lucin: renaming due to simpler scanning (Istate .. found_accept)
|
file | diff | annotate |
| Mon, 20 Jan 2020 11:11:56 +0100 |
lucin: cleanup Istate (doubled code in Istate_Def)
|
file | diff | annotate |
| Fri, 17 Jan 2020 12:37:21 +0100 |
lucin: renaming
|
file | diff | annotate |
| Wed, 15 Jan 2020 11:47:38 +0100 |
preps for IJCAR paper
|
file | diff | annotate |
| Fri, 20 Dec 2019 10:24:52 +0100 |
ok again Test_Isac_Short since last 2 change sets
|
file | diff | annotate |
| Fri, 20 Dec 2019 09:41:11 +0100 |
remove unused fun mk_tac'_, get_form
|
file | diff | annotate |
| Thu, 19 Dec 2019 17:37:25 +0100 |
lucin: unify fun.ids. for locate_input_tactic
|
file | diff | annotate |
| Thu, 19 Dec 2019 16:41:57 +0100 |
cleanup fun solve, shift from Solve --> Step_Solve
|
file | diff | annotate |
| Wed, 18 Dec 2019 15:33:27 +0100 |
prep. intro. of Step
|
file | diff | annotate |
| Mon, 16 Dec 2019 14:03:16 +0100 |
lucin: re-build determine_next_tactic, "ONE ERROR" outcommented
|
file | diff | annotate |
| Sat, 30 Nov 2019 15:43:14 +0100 |
lucin: prep. next_tactic_result, Accept_Tac2 takes ctxt in addition
|
file | diff | annotate |
| Wed, 27 Nov 2019 18:47:26 +0100 |
lucin: push ctxt further into interpreter
|
file | diff | annotate |
| Tue, 26 Nov 2019 17:37:17 +0100 |
lucin: improve readability
|
file | diff | annotate |
| Mon, 25 Nov 2019 16:39:52 +0100 |
lucin: renaming in scanning the parse-tree
|
file | diff | annotate |
| Thu, 07 Nov 2019 10:43:32 +0100 |
lucin: renaming for paper
|
file | diff | annotate |
| Mon, 04 Nov 2019 11:40:29 +0100 |
[Test_Isac] lucin: remove Istate.get_*, unnecessary for record.
|
file | diff | annotate |
| Thu, 31 Oct 2019 10:41:42 +0100 |
lucin: extend Pstate with an additional flag
|
file | diff | annotate |
| Wed, 30 Oct 2019 16:46:05 +0100 |
lucin: remove remaining Pstate exhibiting internal structure
|
file | diff | annotate |
| Wed, 30 Oct 2019 13:59:49 +0100 |
lucin: rule-set for evaluation works in istate
|
file | diff | annotate |
| Wed, 30 Oct 2019 11:02:41 +0100 |
lucin: extend istate with rule-set vor evaluation
|
file | diff | annotate |
| Sun, 27 Oct 2019 12:10:57 +0100 |
lucin: replace Istate.safe by Istate.appy_
|
file | diff | annotate |
| Sat, 19 Oct 2019 14:59:09 +0200 |
lucin: assimilate signatures
|
file | diff | annotate |
| Tue, 01 Oct 2019 10:47:25 +0200 |
lucin: drop unused bool argument in tactic Rewrite*Inst
|
file | diff | annotate |
| Thu, 29 Aug 2019 10:59:57 +0200 |
separate Prog_Tac.thy
|
file | diff | annotate |
| Mon, 26 Aug 2019 17:40:27 +0200 |
rename Isac.thy --> Isac_Knowledge.thy
|
file | diff | annotate |
| Thu, 22 Aug 2019 16:48:04 +0200 |
lucin: rename Script --> Program
|
file | diff | annotate |
| Thu, 22 Aug 2019 12:18:58 +0200 |
lucin: renaming from "script" to "program"
|
file | diff | annotate |
| Thu, 22 Aug 2019 11:26:14 +0200 |
lucin: clarify initialisation of ctxt by ContextC.initialise, initialise'
|
file | diff | annotate |
| Tue, 25 Jun 2019 16:21:18 +0200 |
lucin: adapt tests to new file src/../lucas-interpreter.sml
|
file | diff | annotate |
| Tue, 25 Jun 2019 12:48:24 +0200 |
lucin: rename 3 main functions of lucase-interpreter.sml
|
file | diff | annotate |
| Sat, 01 Jun 2019 11:09:19 +0200 |
[-Test_Isac] funpack: repair errors in test, spot remaining errors
|
file | diff | annotate |
| Mon, 27 May 2019 19:28:40 +0200 |
funpack: failed trial to generalise handling of meths which extend the model of a probl
|
file | diff | annotate |
| Fri, 10 May 2019 15:59:58 +0200 |
funpack: release sequence-relation between method's itm list and partial_function's arg list
|
file | diff | annotate |
| Thu, 28 Feb 2019 12:38:15 +0100 |
remove test, which is unused in demos
|
file | diff | annotate |
| Tue, 22 Jan 2019 11:21:08 +0100 |
[-Test_Isac] funpack: Test_Isac ok until Knowledge
|
file | diff | annotate |
| Tue, 22 Jan 2019 09:33:11 +0100 |
[-Test_Isac] funpack: in programs and spec.terms replace bdv by ''bdv''
|
file | diff | annotate |
| Thu, 08 Mar 2018 07:28:17 +0100 |
TermC: push struct to tests, 3 broken and collected in Test_Isac.
|
file | diff | annotate |
| Thu, 22 Dec 2016 11:36:20 +0100 |
renamed Ctree.ptree --> Ctree.ctree
|
file | diff | annotate |
| Sat, 12 Nov 2016 17:21:43 +0100 |
--- polished LUCAS_INTERPRETER
|
file | diff | annotate |
| Thu, 20 Oct 2016 10:26:29 +0200 |
simplify handling of theorems
|
file | diff | annotate |
| Tue, 18 Oct 2016 12:05:03 +0200 |
back-track after desing error in previous changeset
|
file | diff | annotate |
| Wed, 05 Oct 2016 13:09:54 +0200 |
cleaned tests from autoCalculate' (removed ')
|
file | diff | annotate |
| Mon, 07 Dec 2015 14:10:59 +0100 |
Isabelle2014-->15: closed Thm.thy applied to tests
|
file | diff | annotate |
| Thu, 24 Jul 2014 17:22:21 +0200 |
corrected string_of_thmI, wrong since Isabelle2009-->2011
|
file | diff | annotate |
| Fri, 13 Jun 2014 12:42:15 +0200 |
autoCalculate now parallelized
|
file | diff | annotate |
| Fri, 13 Jun 2014 12:06:38 +0200 |
moved from "Unsynchronized.ref states" to "Synchronized.var states"
|
file | diff | annotate |
| Thu, 21 Nov 2013 18:12:17 +0100 |
Isabelle2013 --> 2013-1: Test_Isac perfect
|
file | diff | annotate |
| Mon, 02 Sep 2013 16:16:08 +0200 |
Test_Isac works again, almost ..
|
file | diff | annotate |
| Thu, 11 Jul 2013 16:58:31 +0200 |
end of improving tests for isac on Isabelle2012
|
file | diff | annotate |
| Wed, 05 Dec 2012 15:56:38 +0100 |
Test_Isac.thy works until "Interpret/mstools.sml"
|
file | diff | annotate |
| Wed, 13 Jun 2012 07:28:39 +0200 |
first dialog sequence for error patterns
|
file | diff | annotate |
| Sat, 17 Mar 2012 11:06:46 +0100 |
uncomment test/../rateq.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Sat, 10 Mar 2012 09:41:09 +0100 |
uncomment test/../biegelinie (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Fri, 23 Sep 2011 13:58:27 +0200 |
tuned
|
file | diff | annotate |
| Fri, 23 Sep 2011 08:30:35 +0200 |
repair ctxt in locate_gen
|
file | diff | annotate |
| Wed, 27 Jul 2011 11:57:46 +0200 |
tuned
|
file | diff | annotate |
| Fri, 22 Jul 2011 15:57:22 +0200 |
intermed: uncomment tests
|
file | diff | annotate |
| Thu, 21 Jul 2011 16:57:21 +0200 |
intermed: uncomment test
|
file | diff | annotate |
| Tue, 17 May 2011 17:38:35 +0200 |
intermed. ctxt ..: ctxt correct after Apply_Method in sub-method
|
file | diff | annotate |
| Wed, 11 May 2011 14:58:07 +0200 |
intermed. ctxt ..: Add_Given doesnt work due to wrong ctxt in Subproblem
|
file | diff | annotate |