| Sun, 09 Oct 2022 07:44:22 +0200 |
eliminate term2str in test/*
|
file | diff | annotate |
| Fri, 07 Oct 2022 20:46:48 +0200 |
follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Tue, 24 May 2022 16:47:31 +0200 |
unify parse 5': improved get_ctxt for appendFormula and CAS-cmd
|
file | diff | annotate |
| Sun, 18 Jul 2021 16:20:32 +0200 |
eliminate ThmC.numerals_to_Free: Test_Isac_Short.thy works with TOODOO s
|
file | diff | annotate |
| Sat, 17 Jul 2021 14:05:28 +0200 |
replace "-*" by "- *" for numerals "*" in test/*
|
file | diff | annotate |
| Sun, 18 Apr 2021 18:30:31 +0200 |
proper test sessions, but with remaining failures;
|
file | diff | annotate |
| Fri, 16 Apr 2021 22:29:23 +0200 |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Fri, 15 May 2020 11:46:43 +0200 |
shift code from Specification to appropriate locations
|
file | diff | annotate |
| Thu, 14 May 2020 13:33:47 +0200 |
rename Specification -> References, contiued
|
file | diff | annotate |
| Fri, 10 Apr 2020 18:32:36 +0200 |
use "UnparseC" for renaming identifiers
|
file | diff | annotate |
| Thu, 09 Apr 2020 17:13:17 +0200 |
separate struct. UnparseC, shift code to ThmC
|
file | diff | annotate |
| Tue, 31 Mar 2020 15:43:33 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Wed, 25 Mar 2020 09:17:05 +0100 |
ONE tactic per step VISIBLE in calculation
|
file | diff | annotate |
| Fri, 20 Mar 2020 19:31:55 +0100 |
collect code for by_tactic..Check_Postcond'
|
file | diff | annotate |
| Wed, 04 Mar 2020 15:38:06 +0100 |
unify copy&paste-code in Sub_Problem.prog_to_tac
|
file | diff | annotate |
| Mon, 24 Feb 2020 17:51:26 +0100 |
prep.: add test-code and test, cleanup
|
file | diff | annotate |
| Mon, 26 Aug 2019 17:40:27 +0200 |
rename Isac.thy --> Isac_Knowledge.thy
|
file | diff | annotate |
| Thu, 22 Aug 2019 11:26:14 +0200 |
lucin: clarify initialisation of ctxt by ContextC.initialise, initialise'
|
file | diff | annotate |
| Fri, 09 Aug 2019 14:04:13 +0200 |
separater structure ContextC
|
file | diff | annotate |
| Wed, 21 Nov 2018 12:32:54 +0100 |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
file | diff | annotate |
| Tue, 28 Aug 2018 13:34:22 +0200 |
Isabelle2017->18: adapt to more rigorous session handling
|
file | diff | annotate |
| Mon, 26 Mar 2018 09:20:09 +0200 |
Rule: Test_Isac works completely
|
file | diff | annotate |
| Fri, 23 Mar 2018 10:14:39 +0100 |
Celem: Test_Isac partially
|
file | diff | annotate |
| Thu, 15 Mar 2018 15:48:52 +0100 |
Celem: tests within imports work, except All_Ctxt
|
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 |
| Wed, 07 Feb 2018 13:06:27 +0100 |
Isabelle2015->17: test setup for ADDTESTS/All_Ctxt, fst error in "ProgLang/termC.sml"
|
file | diff | annotate |
| Wed, 07 Feb 2018 11:21:54 +0100 |
Isabelle2015->17: header in thys dropped
|
file | diff | annotate |
| Sat, 04 Feb 2017 07:20:39 +0100 |
separate structure Stool : SPECIFY_TOOL
|
file | diff | annotate |
| Thu, 22 Dec 2016 10:25:49 +0100 |
--- closed structure Ctree
|
file | diff | annotate |
| Wed, 21 Dec 2016 11:27:22 +0100 |
added structure Ctree : CALC_TREEE
|
file | diff | annotate |
| Mon, 12 Dec 2016 18:08:13 +0100 |
added structure Chead : CALC_HEAD
|
file | diff | annotate |
| Tue, 22 Nov 2016 10:42:21 +0100 |
added structure Math_Engine : MATH_ENGINE
|
file | diff | annotate |
| Tue, 18 Jun 2013 17:51:36 +0200 |
Test_Isac.thy started in Isabelle2012
|
file | diff | annotate |
| Sun, 16 Jun 2013 13:10:32 +0200 |
Isabelle2011 --> 2012 intermediate: find appropriate Isac binary
|
file | diff | annotate |
| Mon, 18 Jul 2011 16:37:30 +0200 |
intermed: make autocalc..CompleteCalc run with x+1=2
|
file | diff | annotate |
| Mon, 18 Jul 2011 09:29:17 +0200 |
intermed: make autocalc..CompleteCalc run with x+1=2
|
file | diff | annotate |
| Sun, 29 May 2011 18:14:43 +0200 |
tuned
|
file | diff | annotate |
| Sun, 29 May 2011 12:53:49 +0200 |
presentation tuned
|
file | diff | annotate |
| Fri, 27 May 2011 12:02:29 +0200 |
added doc-src mlehnfeld
|
file | diff | annotate |
| Sat, 21 May 2011 12:52:59 +0200 |
intermed. ctxt .. FINISHED
|
file | diff | annotate |