| Thu, 15 Mar 2018 10:17:44 +0100 |
separate structure Celem: CALC_ELEMENT, all but Knowledge/
|
file | diff | annotate |
| Fri, 02 Mar 2018 16:19:02 +0100 |
TermC: clean signature, partially
|
file | diff | annotate |
| Fri, 02 Mar 2018 14:19:59 +0100 |
separate structure TermC : TERMC
|
file | diff | annotate |
| Sun, 25 Feb 2018 12:36:23 +0100 |
separate structure Calc : NUMERAL_CALCULATION
|
file | diff | annotate |
| Fri, 23 Feb 2018 07:29:36 +0100 |
separate structure Rewrite : REWRITE
|
file | diff | annotate |
| Wed, 14 Feb 2018 12:20:35 +0100 |
separate structure LTools : LANGUAGE_TOOLS
|
file | diff | annotate |
| Wed, 07 Feb 2018 10:24:16 +0100 |
Isabelle2015->17: session identifiers enforced now
|
file | diff | annotate |
| Sat, 20 Jan 2018 16:53:23 +0100 |
------ Interpret/Interpret.thy builds again
|
file | diff | annotate |
| Mon, 06 Feb 2017 08:52:51 +0100 |
remove warnings "unused" from structures, finished for Interpret/
|
file | diff | annotate |
| Mon, 06 Feb 2017 06:27:31 +0100 |
begin to re-arrange structures in Interpret.thy
|
file | diff | annotate |
| Sat, 21 Jan 2017 14:53:45 +0100 |
--- prep 5 for structure Tac : TACTIC
|
file | diff | annotate |
| Sat, 21 Jan 2017 12:32:32 +0100 |
prep 4 for structure Tac : TACTIC
|
file | diff | annotate |
| Sat, 21 Jan 2017 12:01:30 +0100 |
prep 3 for structure Tac : TACTIC
|
file | diff | annotate |
| Sat, 21 Jan 2017 11:30:18 +0100 |
prep 2 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 14:05:55 +0100 |
clean structure Ctree
|
file | diff | annotate |
| Thu, 22 Dec 2016 11:36:20 +0100 |
renamed Ctree.ptree --> Ctree.ctree
|
file | diff | annotate |
| Thu, 22 Dec 2016 10:25:49 +0100 |
--- closed structure Ctree
|
file | diff | annotate |
| Wed, 21 Dec 2016 08:57:47 +0100 |
added structure Applicable INTERMEDIATELY
|
file | diff | annotate |
| Wed, 14 Dec 2016 09:37:01 +0100 |
added structure Ctree : CALC_TREE
|
file | diff | annotate |
| Mon, 12 Dec 2016 18:08:13 +0100 |
added structure Chead : CALC_HEAD
|
file | diff | annotate |
| Wed, 30 Nov 2016 12:09:24 +0100 |
added structure Rtools : REWRITE_TOOLS
|
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 |
| 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 |