Mon, 18 Sep 2023 10:26:35 +0200 |
wneuper |
prepare 4: shift new code (previous CS was: intermediate I_Model.complete_method)
|
changeset |
files
|
Mon, 18 Sep 2023 08:38:33 +0200 |
wneuper |
prepare 3: shift new code
|
changeset |
files
|
Wed, 30 Aug 2023 06:37:56 +0200 |
wneuper |
prepare 2: I_Model.of_max_variant ready for use in I_Model.complete
|
changeset |
files
|
Tue, 29 Aug 2023 09:04:36 +0200 |
wneuper |
prepare 1 (for PIDE turn 12)
|
changeset |
files
|
Tue, 29 Aug 2023 08:35:46 +0200 |
wneuper |
followup 4: delete old code
|
changeset |
files
|
Sun, 27 Aug 2023 17:56:50 +0200 |
wneuper |
update TODO.md
|
changeset |
files
|
Sun, 27 Aug 2023 17:47:56 +0200 |
wneuper |
rename Refine.*
|
changeset |
files
|
Sun, 27 Aug 2023 16:48:03 +0200 |
wneuper |
followup 3: rename Pre_Conds.* and I_Model.* (eliminate *_TEST as much as possible)
|
changeset |
files
|
Sun, 27 Aug 2023 16:09:04 +0200 |
wneuper |
followup 2: delete old code
|
changeset |
files
|
Sun, 27 Aug 2023 11:19:14 +0200 |
wneuper |
followup 1 (to PIDE turn 11a): eliminate penv
|
changeset |
files
|
Sat, 26 Aug 2023 15:14:24 +0200 |
wneuper |
repair Build_Isac (strange error with isac_test)
|
changeset |
files
|
Sat, 26 Aug 2023 11:37:16 +0200 |
wneuper |
PIDE turn 11a: specify-phase works with 3 new environments from max_variant
|
changeset |
files
|
Sat, 26 Aug 2023 10:51:35 +0200 |
wneuper |
prepare 17: repair Biegelinie formals and accordingly data for Formlise.model
|
changeset |
files
|
Sun, 20 Aug 2023 08:54:01 +0200 |
wneuper |
rollback
|
changeset |
files
|
Sat, 19 Aug 2023 05:06:55 +0200 |
wneuper |
PIDE turn 11: Test_Isac_Short works on env_mode, type env_subst and type env_eval
|
changeset |
files
|
Fri, 18 Aug 2023 18:51:18 +0200 |
wneuper |
prepare 16: delete old code 2, shift feedback_to_string Pre_Conds -> I_Model
|
changeset |
files
|
Thu, 17 Aug 2023 08:01:45 +0200 |
wneuper |
prepare 15: delete old code 1, repair Pre_Conds.check_envs_TEST and check_pos
|
changeset |
files
|
Tue, 15 Aug 2023 17:44:56 +0200 |
wneuper |
Test_Isac_Short without errors
|
changeset |
files
|
Tue, 15 Aug 2023 17:39:06 +0200 |
wneuper |
prepare 14: eliminate Pre_Conds.check in test/*
|
changeset |
files
|
Tue, 15 Aug 2023 12:22:49 +0200 |
wneuper |
prepare 13: Testi_Isac_Short without errors
|
changeset |
files
|
Fri, 04 Aug 2023 23:07:04 +0200 |
wneuper |
//prepare 12: Test_Theory/100-init-.. and 150a-add-.. both work with src/*
|
changeset |
files
|
Fri, 04 Aug 2023 10:46:05 +0200 |
wneuper |
prepare 11: Test_Theory/100-init-rootpbl-NEXT_STEP.sml and 150a-add-.. both work
|
changeset |
files
|
Wed, 26 Jul 2023 11:12:55 +0200 |
wneuper |
rollback
|
changeset |
files
|
Fri, 21 Jul 2023 14:16:57 +0200 |
wneuper |
prepare 10: Minisubpbl/* is in test standard format
|
changeset |
files
|
Thu, 20 Jul 2023 10:24:48 +0200 |
wneuper |
prepare 9: Test_Theory works completely (until Apply_Method)
|
changeset |
files
|
Wed, 19 Jul 2023 11:14:22 +0200 |
wneuper |
prepare 8: Test_Theory works until Tactic Specify_Theory
|
changeset |
files
|
Sat, 15 Jul 2023 17:44:37 +0200 |
wneuper |
prepare 7: extend I_Model.of_max_variant with make_envs_preconds
|
changeset |
files
|
Fri, 14 Jul 2023 12:33:25 +0200 |
wneuper |
prepare 6: repair I_Model.of_max_variant
|
changeset |
files
|
Fri, 14 Jul 2023 10:15:38 +0200 |
wneuper |
better usable descriptor type
|
changeset |
files
|
Fri, 14 Jul 2023 09:49:42 +0200 |
wneuper |
make Test_Isac run on previous changeset
|
changeset |
files
|
Fri, 14 Jul 2023 09:29:49 +0200 |
wneuper |
generalise descriptor type
|
changeset |
files
|
Thu, 13 Jul 2023 18:45:13 +0200 |
wneuper |
generalise use of descriptor type
|
changeset |
files
|
Thu, 13 Jul 2023 17:53:58 +0200 |
wneuper |
repair input-template for type bool
|
changeset |
files
|
Thu, 13 Jul 2023 10:51:16 +0200 |
wneuper |
prepare 5: clarify three environments in the specify-phase, see (*2*) type env_subst
|
changeset |
files
|
Tue, 20 Jun 2023 06:26:18 +0200 |
wneuper |
prepare 4: narrow I_Model.T -- _TEST
|
changeset |
files
|
Sun, 04 Jun 2023 10:12:38 +0200 |
wneuper |
prepare 3a: delete respective test
|
changeset |
files
|
Sat, 03 Jun 2023 16:45:43 +0200 |
wneuper |
prepare 3: clean code
|
changeset |
files
|
Tue, 23 May 2023 08:34:53 +0200 |
wneuper |
prepare 2: adapt LItool.init_pstate to I_Model with Position.T
|
changeset |
files
|
Tue, 23 May 2023 07:56:29 +0200 |
wneuper |
rollback
|
changeset |
files
|
Sat, 29 Apr 2023 16:47:59 +0200 |
wneuper |
prepare 1 PIDE turn 11: eliminate P_Spec.parseitm used by I_Model.Par
|
changeset |
files
|
Sat, 29 Apr 2023 15:53:37 +0200 |
wneuper |
add missing I_Model.OLD_to_TEST to sig
|
changeset |
files
|
Wed, 05 Apr 2023 17:46:25 +0200 |
wneuper |
repair Test_Isac (remove one flaw)
|
changeset |
files
|
Tue, 04 Apr 2023 10:54:12 +0200 |
wneuper |
PIDE turn 10> new handling of variants, Pre_Conds.check_OLD/_TEST, I_Model.is_complete_OLD/_TEST
|
changeset |
files
|
Fri, 31 Mar 2023 12:07:52 +0200 |
wneuper |
//new Pre_Conds.check/_TEST breaks tests, need new signature
|
changeset |
files
|
Wed, 08 Mar 2023 17:47:07 +0100 |
wneuper |
CTbasic_TEST holds I_Model_TEST with Position.T,
|
changeset |
files
|
Tue, 07 Mar 2023 16:06:18 +0100 |
wneuper |
repair previous changeset
|
changeset |
files
|
Tue, 07 Mar 2023 15:38:23 +0100 |
wneuper |
I_Model.init_TEST provides completion as far as reasonable
|
changeset |
files
|
Sun, 05 Mar 2023 08:51:34 +0100 |
wneuper |
rename superfluous *_TEST
|
changeset |
files
|
Sat, 04 Mar 2023 19:06:00 +0100 |
wneuper |
tuned
|
changeset |
files
|
Sat, 04 Mar 2023 19:02:39 +0100 |
wneuper |
PIDE turn 9a: handle empty input correct
|
changeset |
files
|
Mon, 27 Feb 2023 09:45:29 +0100 |
wneuper |
PIDE turn 9: handle empty input, error in Test_VSCode_Example, isabelle@
|
changeset |
files
|
Fri, 24 Feb 2023 16:14:28 +0100 |
wneuper |
PIDE turn 8: reorganise Test_VSCode_Example.thy, etc
|
changeset |
files
|
Wed, 22 Feb 2023 18:40:34 +0100 |
wneuper |
add files
|
changeset |
files
|
Wed, 22 Feb 2023 18:38:56 +0100 |
wneuper |
PIDE turn 7: prepare for Template.show
|
changeset |
files
|
Tue, 21 Feb 2023 15:59:46 +0100 |
wneuper |
PIDE turn 6: feedback with Position.T in MODEL_FOR_INTERACTION
|
changeset |
files
|
Mon, 20 Feb 2023 12:51:17 +0100 |
wneuper |
correct last cs: add files etc
|
changeset |
files
|
Mon, 20 Feb 2023 12:33:23 +0100 |
wneuper |
PIDE turn 5: more structure
|
changeset |
files
|
Sun, 19 Feb 2023 13:03:54 +0100 |
wneuper |
PIDE turn 4: I_Model.init requires other datatype feedback
|
changeset |
files
|
Sun, 19 Feb 2023 10:29:58 +0100 |
wneuper |
PIDE turn 3: hints for input format of terms in Model
|
changeset |
files
|
Thu, 16 Feb 2023 16:20:10 +0100 |
wneuper |
tuned
|
changeset |
files
|