| Thu, 15 Mar 2018 10:17:44 +0100 |
separate structure Celem: CALC_ELEMENT, all but Knowledge/
|
file | diff | annotate |
| Wed, 07 Mar 2018 13:15:21 +0100 |
TermC: clean source file, partially
|
file | diff | annotate |
| Fri, 02 Mar 2018 14:19:59 +0100 |
separate structure TermC : TERMC
|
file | diff | annotate |
| Thu, 22 Feb 2018 17:55:29 +0100 |
LTool: cleanup test file
|
file | diff | annotate |
| Fri, 16 Feb 2018 14:39:29 +0100 |
LTool: cleanup source file
|
file | diff | annotate |
| Wed, 14 Feb 2018 12:20:35 +0100 |
separate structure LTools : LANGUAGE_TOOLS
|
file | diff | annotate |
| Tue, 13 Feb 2018 15:14:55 +0100 |
Isabelle2015->17: "normalize" as identifier causes type clash now, etc
|
file | diff | annotate |
| Sat, 20 Jan 2018 16:35:32 +0100 |
------ print_depth became a configuration option
|
file | diff | annotate |
| Tue, 07 Feb 2017 08:57:42 +0100 |
separate structure Model : MODEL
|
file | diff | annotate |
| Mon, 06 Feb 2017 07:10:35 +0100 |
remove warnings "unused" from structure Specify in ptyps.sml
|
file | diff | annotate |
| Mon, 06 Feb 2017 06:27:31 +0100 |
begin to re-arrange structures in Interpret.thy
|
file | diff | annotate |
| Sat, 04 Feb 2017 07:20:39 +0100 |
separate structure Stool : SPECIFY_TOOL
|
file | diff | annotate |
| Sat, 21 Jan 2017 12:32:32 +0100 |
prep 4 for structure Tac : TACTIC
|
file | diff | annotate |
| Sat, 21 Jan 2017 11:30:18 +0100 |
prep 2 for structure Tac : TACTIC
|
file | diff | annotate |
| Sat, 21 Jan 2017 10:25:19 +0100 |
prep 1 for structure Tac : TACTIC
|
file | diff | annotate |
| Mon, 09 Jan 2017 14:47:24 +0100 |
--- Test_Isac fails, restart stepwise
|
file | diff | annotate |
| Thu, 22 Dec 2016 10:25:49 +0100 |
--- closed structure Ctree
|
file | diff | annotate |
| Mon, 19 Dec 2016 09:02:41 +0100 |
cleaned signature MODEL_SPECIFY
|
file | diff | annotate |
| Sun, 18 Dec 2016 16:27:41 +0100 |
added structure Specify : MODEL_SPECIFY
|
file | diff | annotate |
| Wed, 24 Aug 2016 17:27:54 +0200 |
tuned
|
file | diff | annotate |
| Mon, 07 Dec 2015 11:25:02 +0100 |
Isabelle2014-->15: term_of-->Thm.term_of
|
file | diff | annotate |
| Tue, 14 Apr 2015 14:36:02 +0200 |
print_depth to be replaced by configuration option "ML_print_depth"
|
file | diff | annotate |
| Mon, 04 Aug 2014 17:03:55 +0200 |
CLEANUP since 347cf013dee3 and restored Test_Isac
|
file | diff | annotate |
| Mon, 23 Jun 2014 09:26:22 +0200 |
ad thehier: read only from finally completed knowledge
|
file | diff | annotate |
| Sun, 15 Jun 2014 18:39:59 +0200 |
merged
|
file | diff | annotate |
| Sun, 15 Jun 2014 18:27:23 +0200 |
ad 967c8a1eb6b1 (2,3) thehier: ugly chunk makes Test_Isac run
|
file | diff | annotate |
| Thu, 12 Jun 2014 21:59:15 +0200 |
calls to ML_Context.the_generic_context removed from KEStore.thy because they did not work when called from within a future. However, there are still five instances in other locations yet to be removed.
|
file | diff | annotate |
| Mon, 02 Jun 2014 18:06:27 +0200 |
ad 967c8a1eb6b1 (1): restrict read-access to thehier
|
file | diff | annotate |
| Sat, 31 May 2014 15:53:46 +0200 |
ad 967c8a1eb6b1 (6): switched from 'thehier = Unsynchronized.ref' to Theory_Data
|
file | diff | annotate |
| Sun, 02 Feb 2014 03:09:40 +0100 |
ad 967c8a1eb6b1 (7): remove all code concerned with 'mets = Unsynchronized.ref'
|
file | diff | annotate |
| Sun, 02 Feb 2014 01:15:13 +0100 |
ad 967c8a1eb6b1 (2b): in tests, add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
|
file | diff | annotate |
| Sat, 01 Feb 2014 16:44:45 +0100 |
ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
|
file | diff | annotate |
| Fri, 31 Jan 2014 17:50:50 +0100 |
ad 967c8a1eb6b1 (1): restrict access to 'mets = Unsynchronized'
|
file | diff | annotate |
| Mon, 27 Jan 2014 22:26:51 +0100 |
ad 967c8a1eb6b1 (7): removed all code concerned with 'ptyps = Unsynchronized.ref'
|
file | diff | annotate |
| Mon, 27 Jan 2014 11:09:57 +0100 |
ad 967c8a1eb6b1 (2b): add functions accessing Theory_Data in parallel to those accessing "ptyps = Unsynchronized.ref"
|
file | diff | annotate |
| Sun, 26 Jan 2014 01:37:36 +0100 |
ad 967c8a1eb6b1 (2b): for 'ptyps' add functions accessing Theory_Data in parallel to old ones for 'Unsynchronized.ref' in 'test' folder.
|
file | diff | annotate |
| Sat, 25 Jan 2014 21:06:58 +0100 |
ad 967c8a1eb6b1 (1b): access to \!ptyps further restricted
|
file | diff | annotate |
| Fri, 24 Jan 2014 17:34:17 +0100 |
merged
|
file | diff | annotate |
| Fri, 24 Jan 2014 15:44:22 +0100 |
made read access analogous for !ptyps, !mets and !thehier
|
file | diff | annotate |
| Wed, 22 Jan 2014 23:31:59 +0100 |
ad 967c8a1eb6b1: preparations for step 6 (i.e. switch ptyps to Theory_Data)
|
file | diff | annotate |
| Tue, 21 Jan 2014 00:27:44 +0100 |
ad 967c8a1eb6b1 (2): for 'ptyps' add functions accessing Theory_Data in parallel to the old ones for 'Unsynchronized.ref'.
|
file | diff | annotate |
| Mon, 20 Jan 2014 16:15:34 +0100 |
ad 967c8a1eb6b1 (1b): restrict access...
|
file | diff | annotate |
| Tue, 14 Jan 2014 18:46:56 +0100 |
ad 967c8a1eb6b1 (1a): for 'ptyps' shift types ...
|
file | diff | annotate |
| Tue, 17 Dec 2013 00:40:49 +0000 |
tuned
|
file | diff | annotate |
| Tue, 17 Dec 2013 00:31:59 +0000 |
(1) started limiting access to "ptyps = Unsynchronized.ref"
|
file | diff | annotate |
| Fri, 25 Oct 2013 20:58:28 +0100 |
removed all code concerned with "calclist' = Unsynchronized.ref"
|
file | diff | annotate |
| Thu, 24 Oct 2013 00:02:29 +0100 |
switched from "calclist' = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Thu, 10 Oct 2013 19:16:16 +0100 |
restrict access to "calclist' = Unsynchronized.ref"
|
file | diff | annotate |
| Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
file | diff | annotate |
| Fri, 12 Oct 2012 17:06:58 +0200 |
2011-->2012: ProofContext-->Proof_Context
|
file | diff | annotate |
| Thu, 02 Aug 2012 15:48:57 +0200 |
improved fun insert_fillpats
|
file | diff | annotate |
| Mon, 21 May 2012 07:59:57 +0200 |
added fillpats to thehier
|
file | diff | annotate |
| Wed, 16 May 2012 15:47:22 +0200 |
extended "type met" with errpats
|
file | diff | annotate |
| Wed, 16 May 2012 15:01:47 +0200 |
prep. extend "type met" with errpaty
|
file | diff | annotate |
| Fri, 04 May 2012 17:33:31 +0200 |
prep met ["SignalProcessing", "Z_Transform", "Inverse_sub"]
|
file | diff | annotate |
| Wed, 14 Mar 2012 10:59:36 +0100 |
uncomment test/../eqsystem.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Tue, 13 Mar 2012 15:04:09 +0100 |
uncomment test/../ptyps.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Sat, 10 Sep 2011 10:37:24 +0200 |
method ["PolyEq", "solve_d2_polyeq_pq_equation"] works for jrocnik
|
file | diff | annotate |
| Fri, 13 May 2011 17:19:38 +0200 |
intermed. ctxt ..: x+1=2 now goes until Check_elementwise
|
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 |