| Thu, 20 Feb 2020 11:55:29 +0100 |
prep. cleanup istate/ctxt in Ctree
|
file | diff | annotate |
| Tue, 11 Feb 2020 11:58:45 +0100 |
introduce Step.by_tactic, part 1
|
file | diff | annotate |
| Sat, 08 Feb 2020 17:00:37 +0100 |
replace Chead.calcstate' by Calc.T once
|
file | diff | annotate |
| Sat, 08 Feb 2020 16:33:27 +0100 |
step separated wrt Solve .. Specify
|
file | diff | annotate |
| Sat, 08 Feb 2020 14:44:24 +0100 |
LI: locat_input_term has signature as required
|
file | diff | annotate |
| Sat, 08 Feb 2020 12:41:27 +0100 |
LI: prep. test to re-build locate_input_term
|
file | diff | annotate |
| Fri, 07 Feb 2020 12:36:08 +0100 |
LI: rename Lucin to LI
|
file | diff | annotate |
| Tue, 04 Feb 2020 17:11:54 +0100 |
lucin: rename central structure to Lucin
|
file | diff | annotate |
| Fri, 17 Jan 2020 12:37:21 +0100 |
lucin: renaming
|
file | diff | annotate |
| Mon, 23 Dec 2019 16:58:36 +0100 |
shift code from mathengine-stateless.sml to Step.do_next
|
file | diff | annotate |
| Sat, 21 Dec 2019 18:05:13 +0100 |
lucin: unify do_next postponed
|
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 |
| Tue, 26 Nov 2019 17:06:12 +0100 |
lucin: cleanup ContextC, partially
|
file | diff | annotate |
| Wed, 06 Nov 2019 15:08:27 +0100 |
lucin: args of appy, assy & Co reorganised
|
file | diff | annotate |
| Mon, 04 Nov 2019 11:40:29 +0100 |
[Test_Isac] lucin: remove Istate.get_*, unnecessary for record.
|
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 11:02:41 +0100 |
lucin: extend istate with rule-set vor evaluation
|
file | diff | annotate |
| Mon, 26 Aug 2019 17:40:27 +0200 |
rename Isac.thy --> Isac_Knowledge.thy
|
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 |
| Wed, 24 Jul 2019 11:30:59 +0200 |
lucin: separate interpreter-state and improve type-identifier
|
file | diff | annotate |
| Wed, 03 Jul 2019 15:09:16 +0200 |
lucin: fix Test_Isac, rename aux-funs in lucas-interpreter.
|
file | diff | annotate |
| Tue, 25 Jun 2019 12:48:24 +0200 |
lucin: rename 3 main functions of lucase-interpreter.sml
|
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 |
| Wed, 26 Dec 2018 14:24:05 +0100 |
[-Test_Isac] funpack: further replacement ID::type by char string
|
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 |
| Tue, 13 Feb 2018 15:14:55 +0100 |
Isabelle2015->17: "normalize" as identifier causes type clash now, etc
|
file | diff | annotate |
| Tue, 06 Feb 2018 16:18:43 +0100 |
Isabelle2015->17: transfer changes from src/ to test/
|
file | diff | annotate |
| Thu, 22 Dec 2016 11:36:20 +0100 |
renamed Ctree.ptree --> Ctree.ctree
|
file | diff | annotate |
| Sun, 18 Dec 2016 16:27:41 +0100 |
added structure Specify : MODEL_SPECIFY
|
file | diff | annotate |
| Wed, 30 Nov 2016 13:05:08 +0100 |
finished reformatting Inform
|
file | diff | annotate |
| Thu, 24 Nov 2016 14:33:42 +0100 |
added structure Inform : INPUT_FORMULAS
|
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 |
| Mon, 18 May 2015 14:08:09 +0200 |
outcomment parallelism for simplifying integration of libisabelle
|
file | diff | annotate |
| Mon, 20 Apr 2015 14:18:40 +0200 |
update test/ to Isabelle2014 (~ updates of src/)
|
file | diff | annotate |
| Sat, 26 Jul 2014 14:10:05 +0200 |
added test which identified error in fun getTactic <-- string_of_thmI
|
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 |
| Mon, 10 Mar 2014 21:07:35 +0100 |
user session management now parallel
|
file | diff | annotate |
| Thu, 21 Nov 2013 18:12:17 +0100 |
Isabelle2013 --> 2013-1: Test_Isac perfect
|
file | diff | annotate |
| Mon, 16 Sep 2013 12:20:00 +0200 |
Test_Isac works again, perfectly ..
|
file | diff | annotate |
| Fri, 12 Jul 2013 06:39:55 +0200 |
tuned
|
file | diff | annotate |
| Thu, 11 Jul 2013 16:58:31 +0200 |
end of improving tests for isac on Isabelle2012
|
file | diff | annotate |
| Fri, 21 Jun 2013 11:19:18 +0200 |
Test_Isac.thy without errors on Isabelle2012, intermediate
|
file | diff | annotate |
| Wed, 05 Dec 2012 15:56:38 +0100 |
Test_Isac.thy works until "Interpret/mstools.sml"
|
file | diff | annotate |
| Mon, 30 Jul 2012 16:41:08 +0200 |
findFillpatterns: repaired signature
|
file | diff | annotate |
| Fri, 25 May 2012 16:30:15 +0200 |
added "fun inputFillFormula"
|
file | diff | annotate |
| Fri, 25 May 2012 09:58:20 +0200 |
cleaned "fun generate_inconsistent_rew"
|
file | diff | annotate |
| Thu, 24 May 2012 18:40:07 +0200 |
tuned
|
file | diff | annotate |
| Thu, 24 May 2012 17:13:58 +0200 |
prepared fun inputFillform
|
file | diff | annotate |
| Tue, 22 May 2012 13:40:06 +0200 |
added "fun requestFillformula"
|
file | diff | annotate |
| Tue, 22 May 2012 07:00:53 +0200 |
tuned
|
file | diff | annotate |
| Mon, 21 May 2012 16:56:01 +0200 |
added fun FindFillpatterns
|
file | diff | annotate |
| Thu, 17 May 2012 19:09:48 +0200 |
fun check_error_patterns finished
|
file | diff | annotate |
| Thu, 17 May 2012 12:43:04 +0200 |
fun get_bdv_subst: get a substitution for bound variables from a program
|
file | diff | annotate |