| Sat, 01 Jun 2019 11:09:19 +0200 |
[-Test_Isac] funpack: repair errors in test, spot remaining errors
|
file | diff | annotate |
| Thu, 28 Feb 2019 18:27:29 +0100 |
funpack: drop thms generated by partial_function
|
file | diff | annotate |
| Mon, 26 Mar 2018 07:28:39 +0200 |
Rule: structure pushed to code files
|
file | diff | annotate |
| Thu, 15 Mar 2018 10:17:44 +0100 |
separate structure Celem: CALC_ELEMENT, all but Knowledge/
|
file | diff | annotate |
| Fri, 23 Feb 2018 07:29:36 +0100 |
separate structure Rewrite : REWRITE
|
file | diff | annotate |
| Thu, 22 Dec 2016 10:25:49 +0100 |
--- closed structure Ctree
|
file | diff | annotate |
| Sun, 18 Dec 2016 16:27:41 +0100 |
added structure Specify : MODEL_SPECIFY
|
file | diff | annotate |
| Wed, 30 Nov 2016 12:09:24 +0100 |
added structure Rtools : REWRITE_TOOLS
|
file | diff | annotate |
| Mon, 10 Oct 2016 18:24:14 +0200 |
transport terms in theorems to frontend
|
file | diff | annotate |
| Thu, 06 Oct 2016 17:03:44 +0200 |
PIDE: removed xml for TTY interface of Isabelle2013-2
|
file | diff | annotate |
| Tue, 12 Jan 2016 19:52:22 +0100 |
replace call of MutabelleExtra.thms_of
|
file | diff | annotate |
| Fri, 08 Aug 2014 15:59:20 +0200 |
keep old url for thms at http://www.ist.tugraz.at/projects/isac/
|
file | diff | annotate |
| Thu, 07 Aug 2014 16:28:17 +0200 |
thehier in transition Isabelle2002 --> 2013 finished
|
file | diff | annotate |
| Mon, 04 Aug 2014 17:03:55 +0200 |
CLEANUP since 347cf013dee3 and restored Test_Isac
|
file | diff | annotate |
| Mon, 04 Aug 2014 15:54:57 +0200 |
in thehier replaced Threory.axioms_of by MutabelleExtra.thms_of
|
file | diff | annotate |
| Mon, 28 Jul 2014 17:06:16 +0200 |
ad (a): thehier does not contain sym_thmID theorems anymore
|
file | diff | annotate |
| Sat, 26 Jul 2014 13:39:00 +0200 |
notes and plans on Thm, thmID, thmDeriv
|
file | diff | annotate |
| Thu, 24 Jul 2014 15:18:22 +0200 |
removed the only occurrence of (ill-named) string_of_thm
|
file | diff | annotate |
| Mon, 23 Jun 2014 09:27:04 +0200 |
CLEANUP
|
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 |
| Wed, 11 Jun 2014 16:11:26 +0200 |
ad 967c8a1eb6b1 (2): prepare repair of KEStore_Elems.add_thes
|
file | diff | annotate |
| Thu, 05 Jun 2014 16:41:42 +0200 |
ad 967c8a1eb6b1 (7): remove all code concerned with "thehier = Unsynchronized.ref"
|
file | diff | annotate |
| Wed, 04 Jun 2014 17:41:09 +0200 |
ad 967c8a1eb6b1 (1): adapted tests partially
|
file | diff | annotate |
| Wed, 04 Jun 2014 17:20:40 +0200 |
ad 967c8a1eb6b1 (1): restrict write-access to thehier
|
file | diff | annotate |
| Wed, 04 Jun 2014 16:35:11 +0200 |
ad 967c8a1eb6b1 (1): restrict read-access to thehier finished
|
file | diff | annotate |
| Mon, 17 Mar 2014 08:54:48 +0100 |
re-establish construction of thehier
|
file | diff | annotate |
| Thu, 24 Oct 2013 15:00:44 +0200 |
removed all code concerned with "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Mon, 30 Sep 2013 16:22:07 +0200 |
switched from "ruleset' = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Sun, 22 Sep 2013 18:09:05 +0200 |
add functions accessing Theory_Data in parallel to those accessing "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Thu, 20 Jun 2013 17:53:47 +0200 |
manually completed "thehier" such that insert_errpats, insert_fillpats
|
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 |
| Tue, 24 Apr 2012 17:44:02 +0200 |
generalised store_thm to all knowledge
|
file | diff | annotate |
| Tue, 10 Apr 2012 09:31:21 +0200 |
xml-files created from Knowledge (Isabelle2002 --> 2011)
|
file | diff | annotate |
| Thu, 05 Apr 2012 11:31:56 +0200 |
thydata created (Isabelle2002 --> 2011)
|
file | diff | annotate |
| Mon, 11 Oct 2010 14:22:50 +0200 |
tuned
|
file | diff | annotate |
| Tue, 28 Sep 2010 09:06:56 +0200 |
tuned error and writeln
|
file | diff | annotate |
| Thu, 23 Sep 2010 16:38:25 +0200 |
changed 'writeln' --> 'tracing' in src/ and _NOT_ in test/
|
file | diff | annotate |
| Fri, 10 Sep 2010 11:58:46 +0200 |
intermediate in Knowledge/Isac.thy
|
file | diff | annotate |
| Mon, 23 Aug 2010 11:05:54 +0200 |
updated xmlsrc/* except interface-xml.sml
|
file | diff | annotate |
| Thu, 12 Aug 2010 11:02:32 +0200 |
moved isac + test to final dire-structure
|
file | diff | annotate |