Wed, 30 Aug 2023 06:37:56 +0200 |
prepare 2: I_Model.of_max_variant ready for use in I_Model.complete
|
file | diff | annotate |
Sun, 27 Aug 2023 16:48:03 +0200 |
followup 3: rename Pre_Conds.* and I_Model.* (eliminate *_TEST as much as possible)
|
file | diff | annotate |
Sun, 27 Aug 2023 16:09:04 +0200 |
followup 2: delete old code
|
file | diff | annotate |
Sun, 27 Aug 2023 11:19:14 +0200 |
followup 1 (to PIDE turn 11a): eliminate penv
|
file | diff | annotate |
Fri, 18 Aug 2023 18:51:18 +0200 |
prepare 16: delete old code 2, shift feedback_to_string Pre_Conds -> I_Model
|
file | diff | annotate |
Thu, 17 Aug 2023 08:01:45 +0200 |
prepare 15: delete old code 1, repair Pre_Conds.check_envs_TEST and check_pos
|
file | diff | annotate |
Tue, 15 Aug 2023 12:22:49 +0200 |
prepare 13: Testi_Isac_Short without errors
|
file | diff | annotate |
Fri, 04 Aug 2023 23:07:04 +0200 |
//prepare 12: Test_Theory/100-init-.. and 150a-add-.. both work with src/*
|
file | diff | annotate |
Fri, 04 Aug 2023 10:46:05 +0200 |
prepare 11: Test_Theory/100-init-rootpbl-NEXT_STEP.sml and 150a-add-.. both work
|
file | diff | annotate |
Wed, 26 Jul 2023 11:12:55 +0200 |
rollback
|
file | diff | annotate |
Wed, 19 Jul 2023 11:14:22 +0200 |
prepare 8: Test_Theory works until Tactic Specify_Theory
|
file | diff | annotate |
Sat, 15 Jul 2023 17:44:37 +0200 |
prepare 7: extend I_Model.of_max_variant with make_envs_preconds
|
file | diff | annotate |
Thu, 13 Jul 2023 18:45:13 +0200 |
generalise use of descriptor type
|
file | diff | annotate |
Thu, 13 Jul 2023 10:51:16 +0200 |
prepare 5: clarify three environments in the specify-phase, see (*2*) type env_subst
|
file | diff | annotate |
Tue, 20 Jun 2023 06:26:18 +0200 |
prepare 4: narrow I_Model.T -- _TEST
|
file | diff | annotate |
Tue, 23 May 2023 07:56:29 +0200 |
rollback
|
file | diff | annotate |
Sat, 29 Apr 2023 15:53:37 +0200 |
add missing I_Model.OLD_to_TEST to sig
|
file | diff | annotate |
Tue, 04 Apr 2023 10:54:12 +0200 |
PIDE turn 10> new handling of variants, Pre_Conds.check_OLD/_TEST, I_Model.is_complete_OLD/_TEST
|
file | diff | annotate |
Fri, 31 Mar 2023 12:07:52 +0200 |
//new Pre_Conds.check/_TEST breaks tests, need new signature
|
file | diff | annotate |
Wed, 08 Mar 2023 17:47:07 +0100 |
CTbasic_TEST holds I_Model_TEST with Position.T,
|
file | diff | annotate |
Tue, 07 Mar 2023 16:06:18 +0100 |
repair previous changeset
|
file | diff | annotate |
Tue, 07 Mar 2023 15:38:23 +0100 |
I_Model.init_TEST provides completion as far as reasonable
|
file | diff | annotate |
Mon, 27 Feb 2023 09:45:29 +0100 |
PIDE turn 9: handle empty input, error in Test_VSCode_Example, isabelle@
|
file | diff | annotate |
Wed, 22 Feb 2023 18:38:56 +0100 |
PIDE turn 7: prepare for Template.show
|
file | diff | annotate |
Tue, 21 Feb 2023 15:59:46 +0100 |
PIDE turn 6: feedback with Position.T in MODEL_FOR_INTERACTION
|
file | diff | annotate |
Mon, 20 Feb 2023 12:33:23 +0100 |
PIDE turn 5: more structure
|
file | diff | annotate |
Sun, 19 Feb 2023 13:03:54 +0100 |
PIDE turn 4: I_Model.init requires other datatype feedback
|
file | diff | annotate |
Sun, 19 Feb 2023 10:29:58 +0100 |
PIDE turn 3: hints for input format of terms in Model
|
file | diff | annotate |
Tue, 07 Feb 2023 18:05:15 +0100 |
unify ctxt for ERROR
|
file | diff | annotate |
Tue, 07 Feb 2023 17:25:09 +0100 |
eliminate use of Thy_Info 23: ThyC.get_theory ctxt is mandadory
|
file | diff | annotate |
Sat, 04 Feb 2023 17:00:25 +0100 |
eliminate use of Thy_Info 22: eliminate UnparseC.term, rename "_in_ctxt" -> ""
|
file | diff | annotate |
Sat, 04 Feb 2023 16:49:08 +0100 |
rollback
|
file | diff | annotate |
Sat, 04 Feb 2023 16:20:45 +0100 |
eliminate use of Thy_Info 21: replace Unparse.term, TermC.unparse_ERROR for far off ctxt
|
file | diff | annotate |
Fri, 03 Feb 2023 15:26:19 +0100 |
eliminate use of Thy_Info 18: UnparseC.terms_to_strings --> asms_test
|
file | diff | annotate |
Fri, 03 Feb 2023 12:05:30 +0100 |
eliminate use of Thy_Info 16: eliminate UnparseC.terms in src/*, too
|
file | diff | annotate |
Tue, 31 Jan 2023 11:23:16 +0100 |
cleanup parse #7: eliminate TermC.parseNEW*; cleanup finished
|
file | diff | annotate |
Mon, 30 Jan 2023 12:11:40 +0100 |
cleanup parse #4: eliminate TermC.parse
|
file | diff | annotate |
Sun, 29 Jan 2023 14:31:56 +0100 |
cleanup parse #2: repair error hidden by parse NONE in I_Model.check_single
|
file | diff | annotate |
Sat, 28 Jan 2023 13:21:39 +0100 |
cleanup parse #1: start eliminate parseNEW
|
file | diff | annotate |
Thu, 26 Jan 2023 13:31:07 +0100 |
use exclusively new ContextC.build_while_parsing
|
file | diff | annotate |
Mon, 07 Nov 2022 17:37:20 +0100 |
rename fields in Method_Def.T
|
file | diff | annotate |
Mon, 26 Sep 2022 10:57:53 +0200 |
follow up 2: Problem.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
Wed, 14 Sep 2022 11:33:10 +0200 |
uniform "_PIDE" for functions intermediate in Isabelle/Isac
|
file | diff | annotate |
Wed, 22 Jun 2022 19:26:18 +0200 |
inspect SpecificationC.is_complete
|
file | diff | annotate |
Wed, 22 Jun 2022 16:24:08 +0200 |
rename functions in i-model.sml finished
|
file | diff | annotate |
Tue, 21 Jun 2022 16:04:43 +0200 |
rename functions in i-model.sml
|
file | diff | annotate |
Mon, 20 Jun 2022 18:43:51 +0200 |
merged
|
file | diff | annotate |
Mon, 20 Jun 2022 17:22:26 +0200 |
intermed 2
|
file | diff | annotate |
Mon, 20 Jun 2022 18:37:54 +0200 |
rename functions in o-model.sml
|
file | diff | annotate |
Mon, 20 Jun 2022 11:51:12 +0200 |
initialise state from intermed. example_store
|
file | diff | annotate |
Tue, 16 Nov 2021 18:26:57 +0100 |
unify parse 4: eliminate parse, simple cases
|
file | diff | annotate |
Wed, 29 Sep 2021 19:26:12 +0200 |
unify parse 2: eliminate parseold
|
file | diff | annotate |
Tue, 10 Aug 2021 11:01:18 +0200 |
eliminate ThyC.to_ctxt, use Proof_Context.init_global inline
|
file | diff | annotate |
Tue, 27 Jul 2021 11:21:14 +0200 |
revert previous changeset
|
file | diff | annotate |
Tue, 20 Jul 2021 14:37:56 +0200 |
//reduce the number of TermC.parse*; "//"means: tests broken .
|
file | diff | annotate |
Mon, 19 Jul 2021 15:34:54 +0200 |
ALL const_name replaces (others cannot be replaced)
|
file | diff | annotate |
Wed, 28 Apr 2021 12:38:13 +0200 |
eliminate "handle _ => ..." by \<^try>CARTOUCHE in src/*
|
file | diff | annotate |
Wed, 21 Apr 2021 11:47:30 +0200 |
check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE
|
file | diff | annotate |
Sun, 18 Apr 2021 23:37:59 +0200 |
conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
|
file | diff | annotate |
Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |