| Fri, 07 Oct 2022 20:46:48 +0200 |
follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Mon, 26 Sep 2022 10:57:53 +0200 |
follow up 2: Problem.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Sun, 11 Sep 2022 14:31:15 +0200 |
resolve name clash in get_calc
|
file | diff | annotate |
| Sat, 30 Jul 2022 16:47:45 +0200 |
eliminate global flag Rewrite.trace_on
|
file | diff | annotate |
| Thu, 26 May 2022 12:44:51 +0200 |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
file | diff | annotate |
| Wed, 18 Aug 2021 20:34:41 +0200 |
replace is_const with is_num, ERROR removed
|
file | diff | annotate |
| Wed, 18 Aug 2021 11:35:24 +0200 |
repair test/../root.sml, diff.sml; outcomment NEW errors TOODOO.1
|
file | diff | annotate |
| Wed, 04 Aug 2021 17:34:47 +0200 |
remove comments from (*ML_file ?..?*) in Test_Isac_Short.thy
|
file | diff | annotate |
| Tue, 27 Jul 2021 12:32:43 +0200 |
//test/../diff.sml works again
|
file | diff | annotate |
| Tue, 27 Jul 2021 11:21:14 +0200 |
revert previous changeset
|
file | diff | annotate |
| Tue, 20 Jul 2021 14:37:56 +0200 |
//reduce the number of TermC.parse*; "//"means: tests broken .
|
file | diff | annotate |
| Sun, 18 Jul 2021 18:15:27 +0200 |
merged
|
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 |
| Mon, 21 Jun 2021 15:36:09 +0200 |
more antiquotations for Isabelle/HOL consts/types, without change of semantics;
|
file | diff | annotate |
| Tue, 20 Apr 2021 16:58:44 +0200 |
replace power ^^^ by \<up>
|
file | diff | annotate |
| Mon, 19 Apr 2021 15:02:00 +0200 |
long identifiers for occurences in test/../termC.sml
|
file | diff | annotate |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Sat, 16 May 2020 16:54:39 +0200 |
shift code from Specification to P_Model, rename ids
|
file | diff | annotate |
| Fri, 15 May 2020 11:46:43 +0200 |
shift code from Specification to appropriate locations
|
file | diff | annotate |
| Tue, 12 May 2020 17:42:29 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Mon, 11 May 2020 20:49:27 +0200 |
prep. remove Specify/mstools.sml
|
file | diff | annotate |
| Sat, 02 May 2020 11:36:13 +0200 |
remove Init_Proof, is NOT a tactic
|
file | diff | annotate |
| Wed, 22 Apr 2020 11:06:48 +0200 |
shift Unsynchronized.ref for tracing to respect.struct.
|
file | diff | annotate |
| Tue, 21 Apr 2020 16:53:17 +0200 |
Test_Isac_Short now ok.
|
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 |
| Wed, 01 Apr 2020 10:24:13 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Mon, 24 Feb 2020 17:51:26 +0100 |
prep.: add test-code and test, cleanup
|
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 |
| Wed, 16 Oct 2019 13:37:48 +0200 |
lucin: NEW locate_input_tactic works
|
file | diff | annotate |
| Wed, 02 Oct 2019 16:02:17 +0200 |
lucin: use #> in Program in analogy to #> in Isabelle/ML
|
file | diff | annotate |
| Tue, 01 Oct 2019 10:47:25 +0200 |
lucin: drop unused bool argument in tactic Rewrite*Inst
|
file | diff | annotate |
| Wed, 18 Sep 2019 12:15:59 +0200 |
tests run in Test_Isac with ML_system_64 = "true", still exception Size
|
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 |
| 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 |
| Thu, 08 Mar 2018 07:28:17 +0100 |
TermC: push struct to tests, 3 broken and collected in Test_Isac.
|
file | diff | annotate |
| Sun, 25 Feb 2018 10:19:18 +0100 |
Rewrite: clean tests
|
file | diff | annotate |
| Thu, 27 Oct 2016 10:48:10 +0200 |
rename get_calculation* to adhoc_thm*
|
file | diff | annotate |
| Thu, 20 Oct 2016 10:26:29 +0200 |
simplify handling of theorems
|
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 |
| 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, 24 Oct 2013 17:24:47 +0200 |
removed "rulelist'" also from ~~/test/Tools/isac/*
|
file | diff | annotate |
| Mon, 30 Sep 2013 16:22:07 +0200 |
switched from "ruleset' = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Mon, 02 Sep 2013 16:16:08 +0200 |
Test_Isac works again, almost ..
|
file | diff | annotate |
| Wed, 05 Dec 2012 15:56:38 +0100 |
Test_Isac.thy works until "Interpret/mstools.sml"
|
file | diff | annotate |
| Sun, 14 Oct 2012 21:26:02 +0200 |
2011-->2012: "isabelle usedir -b HOL Isac" works
|
file | diff | annotate |
| Tue, 31 Jul 2012 15:16:47 +0200 |
prepared for fun stepToErrorPatterns
|
file | diff | annotate |
| Wed, 14 Mar 2012 17:12:43 +0100 |
uncomment test/../rootrateq.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Mon, 14 Mar 2011 16:50:44 +0100 |
intermed.update Isabelle2011: tests finished...
|
file | diff | annotate |
| Thu, 10 Mar 2011 17:05:09 +0100 |
intermed.update Isabelle2011: Not --> HOL.Not
|
file | diff | annotate |