| Sun, 04 Apr 2021 12:29:42 +0200 |
separate session Specify
|
file | diff | annotate |
| Wed, 07 Oct 2020 09:45:07 +0200 |
tuned
|
file | diff | annotate |
| Wed, 07 Oct 2020 09:31:10 +0200 |
Isabelle2019->20: adapt to new session requirements continued
|
file | diff | annotate |
| Wed, 29 Apr 2020 12:30:51 +0200 |
prep. separation of check Applicable between specify-phase and solve-phase
|
file | diff | annotate |
| Tue, 28 Apr 2020 17:50:18 +0200 |
separate struct.Thy_Present, rename Thy_Html to Thy_Write
|
file | diff | annotate |
| Tue, 28 Apr 2020 16:51:36 +0200 |
separate struct.Thy_Read
|
file | diff | annotate |
| Fri, 24 Apr 2020 08:51:05 +0200 |
separate struct.Error_Pattern, rename identifiers
|
file | diff | annotate |
| Thu, 23 Apr 2020 09:29:56 +0200 |
separate struct. Derive
|
file | diff | annotate |
| Thu, 09 Apr 2020 11:30:58 +0200 |
rename file according to previous change set
|
file | diff | annotate |
| Sat, 07 Mar 2020 15:37:37 +0100 |
further separate specify- and solve-phase
|
file | diff | annotate |
| Wed, 04 Mar 2020 15:38:06 +0100 |
unify copy&paste-code in Sub_Problem.prog_to_tac
|
file | diff | annotate |
| Mon, 24 Feb 2020 17:51:26 +0100 |
prep.: add test-code and test, cleanup
|
file | diff | annotate |
| Tue, 04 Feb 2020 17:11:54 +0100 |
lucin: rename central structure to Lucin
|
file | diff | annotate |
| Thu, 19 Dec 2019 12:40:17 +0100 |
lucin: various investigations (a chaos change set)
|
file | diff | annotate |
| Wed, 18 Dec 2019 15:33:27 +0100 |
prep. intro. of Step
|
file | diff | annotate |
| Tue, 17 Dec 2019 16:31:46 +0100 |
lucin: shift Istate into Interpret/ from MathEngBasic
|
file | diff | annotate |
| Sat, 14 Dec 2019 13:36:40 +0100 |
remove tracing, which interfere with current investigations
|
file | diff | annotate |
| Thu, 12 Dec 2019 10:09:29 +0100 |
lucin: cleanup fun interpret_leaf
|
file | diff | annotate |
| Sat, 30 Nov 2019 17:03:49 +0100 |
lucin: code cleanup
|
file | diff | annotate |
| Sat, 30 Nov 2019 15:43:14 +0100 |
lucin: prep. next_tactic_result, Accept_Tac2 takes ctxt in addition
|
file | diff | annotate |
| Thu, 31 Oct 2019 13:48:06 +0100 |
tuned
|
file | diff | annotate |
| Thu, 31 Oct 2019 10:41:42 +0100 |
lucin: extend Pstate with an additional flag
|
file | diff | annotate |
| Wed, 30 Oct 2019 16:46:05 +0100 |
lucin: remove remaining Pstate exhibiting internal structure
|
file | diff | annotate |
| Fri, 25 Oct 2019 16:07:15 +0200 |
lucin: adopt Poly/ML warnings in lucas-interpreter.sml
|
file | diff | annotate |
| Sat, 19 Oct 2019 18:19:16 +0200 |
lucin: introduce interpreter-state to appy & Co
|
file | diff | annotate |
| Sat, 19 Oct 2019 14:07:27 +0200 |
tuned
|
file | diff | annotate |
| Thu, 17 Oct 2019 13:17:48 +0200 |
lucin: cleanup args in lucas-interpreter, preps
|
file | diff | annotate |
| Wed, 28 Aug 2019 11:21:26 +0200 |
reorganised MathEngine/ BridgeLibisabelle/
|
file | diff | annotate |
| Tue, 27 Aug 2019 18:03:33 +0200 |
assign Input_Descript to Specify/-phase
|
file | diff | annotate |
| Tue, 27 Aug 2019 11:59:48 +0200 |
separate Specify/ from Interpret/
|
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 09:32:17 +0200 |
lucin: improve signature of "fun locate_input_tactic"
|
file | diff | annotate |
| Mon, 24 Jun 2019 14:02:39 +0200 |
[-Test_Isac] lucin: shift "find next tactic" into lucas-interpreter.sml
|
file | diff | annotate |
| Wed, 21 Nov 2018 12:32:54 +0100 |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
file | diff | annotate |
| Tue, 07 Feb 2017 08:57:42 +0100 |
separate structure Model : MODEL
|
file | diff | annotate |
| Mon, 06 Feb 2017 09:06:35 +0100 |
improved CLEANUP
|
file | diff | annotate |
| Mon, 06 Feb 2017 09:00:32 +0100 |
tuned
|
file | diff | annotate |
| Sat, 04 Feb 2017 07:20:39 +0100 |
separate structure Stool : SPECIFY_TOOL
|
file | diff | annotate |
| Sat, 21 Jan 2017 10:25:19 +0100 |
prep 1 for structure Tac : TACTIC
|
file | diff | annotate |
| Wed, 18 Jan 2017 09:09:04 +0100 |
begin to divide structure Ctree
|
file | diff | annotate |
| Fri, 06 Jan 2017 14:48:20 +0100 |
further preparation for separating ctree-basic.sml
|
file | diff | annotate |
| Wed, 28 Dec 2016 13:07:17 +0100 |
replaced ctree.sml by basic-ctree.sml before separation
|
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 |
| Wed, 30 Nov 2016 12:09:24 +0100 |
added structure Rtools : REWRITE_TOOLS
|
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 |
| Thu, 21 Nov 2013 11:17:42 +0100 |
Isabelle2013 --> 2013-1: remove left-over legacy "uses" "axiom"
|
file | diff | annotate |
| Sun, 16 Jun 2013 12:31:41 +0200 |
Isabelle2011 --> 2012 intermediate
|
file | diff | annotate |
| Fri, 12 Oct 2012 17:06:58 +0200 |
2011-->2012: ProofContext-->Proof_Context
|
file | diff | annotate |
| Wed, 23 Mar 2011 17:20:39 +0100 |
make Test_Isac.thy run in jEdit; intermed.
|
file | diff | annotate |
| Tue, 01 Mar 2011 15:23:59 +0100 |
intermed.update to Isabelle2011: test/../syntax added
|
file | diff | annotate |