| Thu, 22 Aug 2019 16:48:04 +0200 |
lucin: rename Script --> Program
|
file | diff | annotate |
| Thu, 22 Aug 2019 10:27:02 +0200 |
shift e_ctxt Selem. --> ContextC.
|
file | diff | annotate |
| Tue, 13 Aug 2019 09:19:33 +0200 |
[Text_Isac/../inverse_z_transform.sml] lucin: prep. "fun associate" for sig. locate_input_tactic
|
file | diff | annotate |
| Fri, 09 Aug 2019 14:04:13 +0200 |
separater structure ContextC
|
file | diff | annotate |
| Wed, 24 Jul 2019 11:30:59 +0200 |
lucin: separate interpreter-state and improve type-identifier
|
file | diff | annotate |
| Wed, 24 Jul 2019 10:35:19 +0200 |
lucin: improve type-identifiers for signatures
|
file | diff | annotate |
| Tue, 25 Jun 2019 12:48:24 +0200 |
lucin: rename 3 main functions of lucase-interpreter.sml
|
file | diff | annotate |
| Mon, 31 Dec 2018 14:49:16 +0100 |
[-Test_Isac] add an overlooked structure
|
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, 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 |
| 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 |
| Tue, 07 Feb 2017 08:57:42 +0100 |
separate structure Model : MODEL
|
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 |
| Thu, 02 Feb 2017 06:50:47 +0100 |
remove warnings at the cost of opening structures
|
file | diff | annotate |
| Thu, 02 Feb 2017 06:32:30 +0100 |
tuned
|
file | diff | annotate |
| Thu, 02 Feb 2017 06:28:43 +0100 |
finished separate structure Tac : TACTIC
|
file | diff | annotate |
| Sat, 21 Jan 2017 15:13:43 +0100 |
--- prep 5a for structure Tac : TACTIC
|
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 |
| 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 |
| Wed, 28 Dec 2016 11:14:04 +0100 |
added signature SOLVE
|
file | diff | annotate |
| Wed, 28 Dec 2016 08:57:00 +0100 |
clean structure Applicable
|
file | diff | annotate |
| Tue, 27 Dec 2016 17:43:12 +0100 |
demo ERROR: declare [[ML_print_depth = 999]] kills Isabelle/Isac
|
file | diff | annotate |
| Tue, 27 Dec 2016 13:20:33 +0100 |
clean structure Ctree continued
|
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 |
| Mon, 19 Dec 2016 10:37:44 +0100 |
renamed structure to Generate : GENERATE_CALC_TREE
|
file | diff | annotate |
| Sun, 18 Dec 2016 16:27:41 +0100 |
added structure Specify : MODEL_SPECIFY
|
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 |
| 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:25:02 +0100 |
Isabelle2014-->15: term_of-->Thm.term_of
|
file | diff | annotate |
| Mon, 07 Dec 2015 10:17:08 +0100 |
sabelle2014-->15: cterm_of-->Thm.global_cterm_of
|
file | diff | annotate |
| Thu, 24 Oct 2013 17:24:47 +0200 |
removed "rulelist'" also from ~~/test/Tools/isac/*
|
file | diff | annotate |
| Thu, 24 Oct 2013 15:00:44 +0200 |
removed all code concerned with "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Fri, 12 Oct 2012 17:06:58 +0200 |
2011-->2012: ProofContext-->Proof_Context
|
file | diff | annotate |
| Fri, 12 Oct 2012 16:03:07 +0200 |
2011-->2012:
|
file | diff | annotate |
| Sat, 17 Mar 2012 11:06:46 +0100 |
uncomment test/../rateq.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Sat, 07 Jan 2012 10:06:06 +0100 |
invisible changes in calculations are possible now.
|
file | diff | annotate |
| Sat, 21 May 2011 12:52:59 +0200 |
intermed. ctxt .. FINISHED
|
file | diff | annotate |
| Fri, 20 May 2011 14:49:07 +0200 |
tuned
|
file | diff | annotate |
| Sun, 15 May 2011 12:36:29 +0200 |
tuned
|
file | diff | annotate |
| Sun, 15 May 2011 11:32:41 +0200 |
intermed. ctxt ..: checked all occurrences of ProofContext.init_global
|
file | diff | annotate |
| Wed, 11 May 2011 16:51:30 +0200 |
intermed. ctxt ..: added ctxt to Subproblem'
|
file | diff | annotate |
| Wed, 11 May 2011 07:28:13 +0200 |
tuned
|
file | diff | annotate |
| Thu, 05 May 2011 09:23:32 +0200 |
tuned
|
file | diff | annotate |
| Mon, 18 Apr 2011 14:43:26 +0200 |
tuned
|
file | diff | annotate |
| Sat, 16 Apr 2011 10:19:45 +0200 |
Apply_Method transfers ctxt from specification to interpretation
|
file | diff | annotate |
| Fri, 15 Apr 2011 17:07:34 +0200 |
intermed. ctxt integration - assumptions now in context
|
file | diff | annotate |
| Fri, 08 Apr 2011 15:16:08 +0200 |
intermed. context integration: parse replaced in some cases
|
file | diff | annotate |