Sat, 22 Jun 2019 13:15:52 +0200 |
funpack: repair remaining test/../partial_fractions.sml, inverse_z_transform.sml
|
file | diff | annotate |
Thu, 21 Mar 2019 17:51:18 +0100 |
[-Test_Isac] extend "is_polyexp (Const _) = true" for AA
|
file | diff | annotate |
Tue, 13 Feb 2018 15:14:55 +0100 |
Isabelle2015->17: "normalize" as identifier causes type clash now, etc
|
file | diff | annotate |
Fri, 09 Feb 2018 11:45:53 +0100 |
Isabelle2015->17: applied 172b53399454 (on src/) on test/ too
|
file | diff | annotate |
Wed, 07 Feb 2018 15:00:37 +0100 |
Isabelle2015->17: new negation "~ " --> "<not> "
|
file | diff | annotate |
Thu, 22 Dec 2016 11:36:20 +0100 |
renamed Ctree.ptree --> Ctree.ctree
|
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 |
Fri, 08 May 2015 15:43:15 +0200 |
Isabelle201302 --> Isabelle2014: negative numbers' representation changed
|
file | diff | annotate |
Fri, 08 May 2015 15:38:28 +0200 |
Isabelle201302 --> Isabelle2014: delete a test which is unclear how worked before
|
file | diff | annotate |
Thu, 31 Jul 2014 14:21:49 +0200 |
added test going down to derivation of user-input
|
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 |
Tue, 01 Jul 2014 16:38:03 +0200 |
update test on error f8d44cb86330
|
file | diff | annotate |
Sun, 22 Jun 2014 15:22:30 +0200 |
CLEANUP since cf8879216db3
|
file | diff | annotate |
Sun, 22 Jun 2014 14:58:51 +0200 |
ad thehier: update Test_Isac to previous changeset
|
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 |
Sat, 31 May 2014 15:09:33 +0200 |
details on 632d2ecab96f: error (from <NEXT> on new Worksheet)
|
file | diff | annotate |
Sun, 04 May 2014 14:02:23 +0200 |
error (from <NEXT> on new Worksheet) related to thehier
|
file | diff | annotate |
Thu, 21 Nov 2013 18:12:17 +0100 |
Isabelle2013 --> 2013-1: Test_Isac perfect
|
file | diff | annotate |
Thu, 11 Jul 2013 16:58:31 +0200 |
end of improving tests for isac on Isabelle2012
|
file | diff | annotate |
Fri, 12 Oct 2012 17:06:58 +0200 |
2011-->2012: ProofContext-->Proof_Context
|
file | diff | annotate |
Thu, 05 Apr 2012 16:53:43 +0200 |
renamed ID "inverse" to "Inverse" (Isabelle2002 --> 2011)
|
file | diff | annotate |
Sat, 17 Mar 2012 11:06:46 +0100 |
uncomment test/../rateq.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
Thu, 22 Sep 2011 14:24:34 +0200 |
made Build_Inverse_Z_Transform.thy run
|
file | diff | annotate |
Thu, 28 Jul 2011 11:27:04 +0200 |
completed praktikum
|
file | diff | annotate |
Tue, 19 Jul 2011 09:53:30 +0200 |
Automated merge with https://intra.ist.tugraz.at/hg/isa/
|
file | diff | annotate |
Tue, 19 Jul 2011 09:43:01 +0200 |
intermed: uncomment tests with CompleteCalc
|
file | diff | annotate |
Mon, 18 Jul 2011 16:42:26 +0200 |
finished: make autocalc..CompleteCalc run with x+1=2
|
file | diff | annotate |
Mon, 18 Jul 2011 16:39:22 +0200 |
tuned
|
file | diff | annotate |
Mon, 18 Jul 2011 16:37:30 +0200 |
intermed: make autocalc..CompleteCalc run with x+1=2
|
file | diff | annotate |
Tue, 28 Jun 2011 15:14:00 +0200 |
intermed: make autocalc..CompleteCalc run with x+1=2
|
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 |
Tue, 03 May 2011 16:20:55 +0200 |
provided all "x+1=2" with typeconstraint real ("equality" is just bool)
|
file | diff | annotate |
Fri, 08 Apr 2011 15:16:08 +0200 |
intermed. context integration: parse replaced in some cases
|
file | diff | annotate |
Wed, 06 Apr 2011 18:01:02 +0200 |
intermed. context introduction to specification phase
|
file | diff | annotate |
Mon, 04 Apr 2011 11:05:07 +0200 |
intermed. context integration appl_add does not work
|
file | diff | annotate |
Wed, 23 Mar 2011 17:20:39 +0100 |
make Test_Isac.thy run in jEdit; intermed.
|
file | diff | annotate |
Sat, 19 Mar 2011 15:03:36 +0100 |
intermed. usecase Diophant: usecase1 shifted into test/../mathengine.sml
|
file | diff | annotate |
Thu, 10 Mar 2011 17:05:09 +0100 |
intermed.update Isabelle2011: Not --> HOL.Not
|
file | diff | annotate |
Wed, 03 Nov 2010 11:54:53 +0100 |
----- final tests go through (test/../interface.sml)
|
file | diff | annotate |
Wed, 03 Nov 2010 09:45:59 +0100 |
check 'autoCalculate 1 CompleteCalc': works for test/../integrate.sml
|
file | diff | annotate |
Mon, 11 Oct 2010 13:31:22 +0200 |
removed all ".thy" in src/ and test/
|
file | diff | annotate |
Tue, 28 Sep 2010 09:06:56 +0200 |
tuned error and writeln
|
file | diff | annotate |
Mon, 30 Aug 2010 14:35:51 +0200 |
renamed test/* according to src/*
|
file | diff | annotate | base |