| 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 |
| Tue, 18 Oct 2016 12:05:03 +0200 |
back-track after desing error in previous changeset
|
file | diff | annotate |
| Mon, 10 Oct 2016 18:24:14 +0200 |
transport terms in theorems to frontend
|
file | diff | annotate |
| Mon, 07 Dec 2015 11:32:12 +0100 |
Isabelle2014-->15: rem_thm-->Thm.rep_thm
|
file | diff | annotate |
| Mon, 07 Dec 2015 10:52:07 +0100 |
Isabelle2014-->15: Thm.thy is not open anymore, further funs qualified
|
file | diff | annotate |
| Mon, 07 Dec 2015 10:01:49 +0100 |
Isabelle2014-->15: prop_of-->Thm.prop_of
|
file | diff | annotate |
| Thu, 23 Oct 2014 16:40:58 +0200 |
Isabelle2002 --> 2013: reactivated context_thy
|
file | diff | annotate |
| Thu, 31 Jul 2014 14:32:05 +0200 |
collected updates since changeset 066b35da6c97
|
file | diff | annotate |
| Thu, 31 Jul 2014 14:15:41 +0200 |
ad (b): lookup for sym_thmID directly from Isabelle using sym_thm
|
file | diff | annotate |
| Sun, 22 Jun 2014 14:47:36 +0200 |
ad thehier: removed theory' = Unsychronized.ref
|
file | diff | annotate |
| Sun, 22 Jun 2014 14:32:51 +0200 |
ad thehier: add funs grouping thys handled in Isac
|
file | diff | annotate |
| Thu, 19 Jun 2014 07:51:40 +0200 |
ad 967c8a1eb6b1 (7) thehier: remove code superfluous by last changeset
|
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 17:56:53 +0200 |
finished transition Isabelle2011-->2013
|
file | diff | annotate |
| Mon, 17 Mar 2014 08:54:48 +0100 |
re-establish construction of thehier
|
file | diff | annotate |
| Thu, 21 Nov 2013 11:17:42 +0100 |
Isabelle2013 --> 2013-1: remove left-over legacy "uses" "axiom"
|
file | diff | annotate |
| Thu, 24 Oct 2013 15:00:44 +0200 |
removed all code concerned with "ruleset' = 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 |
| 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 |
| Mon, 22 Jul 2013 13:52:18 +0200 |
--- Test_Isac.thy runs all tests
|
file | diff | annotate |
| Fri, 21 Jun 2013 17:49:24 +0200 |
Test_Isac.thy without errors on Isabelle2012, rewtools.sml:
|
file | diff | annotate |
| Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
file | diff | annotate |
| Tue, 31 Jul 2012 15:16:47 +0200 |
prepared for fun stepToErrorPatterns
|
file | diff | annotate |
| Thu, 24 May 2012 17:13:58 +0200 |
prepared fun inputFillform
|
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 |
| Tue, 20 Mar 2012 15:32:17 +0100 |
intermed. fun the_hier, build thy-hierarchy
|
file | diff | annotate |
| Mon, 20 Feb 2012 18:18:03 +0100 |
Jan finished his work
|
file | diff | annotate |
| Sun, 19 Feb 2012 10:03:51 +0100 |
protocol dmeindl, decomment Test_Isac
|
file | diff | annotate |
| Sat, 26 Feb 2011 11:34:08 +0100 |
intermed.update to Isabelle2011
|
file | diff | annotate |
| Mon, 21 Feb 2011 19:40:36 +0100 |
part.update Isabelle2011
|
file | diff | annotate |
| Thu, 28 Oct 2010 09:24:47 +0200 |
intermed. repair thehier, the hierarchy of thy/thm for access by isac.
|
file | diff | annotate |
| Mon, 11 Oct 2010 13:31:22 +0200 |
removed all ".thy" in src/ and test/
|
file | diff | annotate |
| Sat, 09 Oct 2010 16:03:49 +0200 |
repaired Print_Mode.setmp [] ((Syntax.string_of_term
|
file | diff | annotate |
| Wed, 06 Oct 2010 15:12:41 +0200 |
intermed. test/../integrate.sml in -- me method [diff,integration] --
|
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 |
| Fri, 03 Sep 2010 17:19:20 +0200 |
updated Knowledge/Rational
|
file | diff | annotate |
| Wed, 01 Sep 2010 15:17:43 +0200 |
fixed all @{thm } in src+test
|
file | diff | annotate |
| Tue, 31 Aug 2010 16:00:13 +0200 |
num_str --> num_str @{thm
|
file | diff | annotate |
| Wed, 25 Aug 2010 16:20:07 +0200 |
renamed isac's directories and Build_Isac.thy
|
file | diff | annotate | base |