| Mon, 19 Apr 2021 19:55:31 +0200 |
no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
|
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 |
| Sun, 18 Apr 2021 18:30:31 +0200 |
proper test sessions, but with remaining failures;
|
file | diff | annotate |
| Fri, 16 Apr 2021 22:29:23 +0200 |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:37:10 +0100 |
step 3.2: prep.data for start of specify-phase
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:22:24 +0100 |
adopt new theory identifier also in comments
|
file | diff | annotate |
| Mon, 26 Oct 2020 13:52:26 +0100 |
copy Outer_Syntax.command..spark_open as model for Isac Calculation
|
file | diff | annotate |
| Thu, 22 Oct 2020 15:40:41 +0200 |
complete imports to Test_Isac*
|
file | diff | annotate |
| Fri, 17 Jul 2020 11:42:20 +0200 |
cleanup Test_Parse*, start parsers for keyword ISAC
|
file | diff | annotate |
| Mon, 29 Jun 2020 17:27:34 +0200 |
new test me' doesn't overload jEdit buffers
|
file | diff | annotate |
| Wed, 03 Jun 2020 11:25:19 +0200 |
follow 2 ancient updates of Library.ML
|
file | diff | annotate |
| Tue, 19 May 2020 12:33:35 +0200 |
adapt test/../Specify/* to new files in src/../Specify/*
|
file | diff | annotate |
| Fri, 15 May 2020 19:31:04 +0200 |
shift code from Specification to References, separate References_Def
|
file | diff | annotate |
| Thu, 14 May 2020 13:33:47 +0200 |
rename Specification -> References, contiued
|
file | diff | annotate |
| Thu, 14 May 2020 09:30:40 +0200 |
start renaming Specification -> References;
|
file | diff | annotate |
| Wed, 13 May 2020 11:34:05 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Tue, 12 May 2020 07:27:21 +0200 |
remove Specify/mstools.sml
|
file | diff | annotate |
| Mon, 11 May 2020 20:49:27 +0200 |
prep. remove Specify/mstools.sml
|
file | diff | annotate |
| Sun, 10 May 2020 17:26:36 +0200 |
cleanup generate.sml, model.sml
|
file | diff | annotate |
| Sun, 10 May 2020 13:16:56 +0200 |
investigate I_Model
|
file | diff | annotate |
| Tue, 05 May 2020 09:07:36 +0200 |
separate struc.Formalise
|
file | diff | annotate |
| Mon, 04 May 2020 13:27:45 +0200 |
remove unused code
|
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 |
| Wed, 29 Apr 2020 09:03:01 +0200 |
comments on relation between files.
|
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 15:31:49 +0200 |
assign code from Rtools to appropriate struct.s
|
file | diff | annotate |
| Mon, 27 Apr 2020 12:36:21 +0200 |
separate struct.Subst, rename idenfitiers
|
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 |
| Wed, 22 Apr 2020 11:23:30 +0200 |
rename file according to struct.; start renaming with "Spec"
|
file | diff | annotate |
| Mon, 20 Apr 2020 15:54:19 +0200 |
separate Check_Unique, an exercise in higher order funs
|
file | diff | annotate |
| Wed, 15 Apr 2020 11:37:43 +0200 |
cleanup
|
file | diff | annotate |
| Fri, 10 Apr 2020 15:02:50 +0200 |
rename directory CalcElements to BaseDefinitions
|
file | diff | annotate |
| Fri, 10 Apr 2020 14:46:55 +0200 |
rearrange code for ThmC
|
file | diff | annotate |
| Thu, 09 Apr 2020 11:21:53 +0200 |
separate struct. ThmC, Error_Fill_Def; unite error-pattern and fill-pattern
|
file | diff | annotate |
| Wed, 01 Apr 2020 18:54:03 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Wed, 01 Apr 2020 10:24:13 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Sat, 07 Mar 2020 17:11:55 +0100 |
cleanup LItool, begin
|
file | diff | annotate |
| Sat, 07 Mar 2020 15:37:37 +0100 |
further separate specify- and solve-phase
|
file | diff | annotate |
| Sat, 07 Mar 2020 11:54:13 +0100 |
cleanup ctxt: replace Ctree.update_ctxt by Ctree.cupdate_problem
|
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 |
| Fri, 07 Feb 2020 12:36:08 +0100 |
LI: rename Lucin to LI
|
file | diff | annotate |
| Tue, 04 Feb 2020 17:11:54 +0100 |
lucin: rename central structure to Lucin
|
file | diff | annotate |
| Wed, 22 Jan 2020 11:20:54 +0100 |
lucin: tests towards simpl. Lucin.scan*
|
file | diff | annotate |
| Fri, 17 Jan 2020 13:14:11 +0100 |
lucin: introduce Calc.T and Program.T
|
file | diff | annotate |
| Wed, 15 Jan 2020 12:12:44 +0100 |
lucin: rename fun *2 to fun * with expectation to unify fun * with fun *1
|
file | diff | annotate |
| Mon, 23 Dec 2019 15:41:36 +0100 |
separate Step_Specify, Step_Solve, Step for do_next and by_tactic
|
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 |
| Fri, 29 Nov 2019 15:22:29 +0100 |
lucin: fun determine_next_tactic gets envisaged arguments
|
file | diff | annotate |
| Wed, 27 Nov 2019 18:47:26 +0100 |
lucin: push ctxt further into interpreter
|
file | diff | annotate |
| Thu, 07 Nov 2019 10:43:32 +0100 |
lucin: renaming for paper
|
file | diff | annotate |
| Wed, 06 Nov 2019 15:08:27 +0100 |
lucin: args of appy, assy & Co reorganised
|
file | diff | annotate |
| Sat, 26 Oct 2019 13:03:16 +0200 |
separate common base for Specify and Interpret
|
file | diff | annotate |
| Thu, 17 Oct 2019 13:17:48 +0200 |
lucin: cleanup args in lucas-interpreter, preps
|
file | diff | annotate |
| Wed, 18 Sep 2019 16:28:49 +0200 |
tests run in Test_Isac with ML_system_64 = "true"
|
file | diff | annotate |
| Wed, 18 Sep 2019 12:15:59 +0200 |
tests run in Test_Isac with ML_system_64 = "true", still exception Size
|
file | diff | annotate |
| Tue, 17 Sep 2019 10:25:24 +0200 |
tests run in Text_Isac_Short.thy in x86_64_32 mode of Poly/ML 5.8
|
file | diff | annotate |
| Mon, 16 Sep 2019 20:40:33 +0200 |
[Test_Isac] notes and out-commenting in tests
|
file | diff | annotate |
| Fri, 13 Sep 2019 18:35:51 +0200 |
lucin: cleanup thys in ProgLang, in particular Aut_Prog.thy
|
file | diff | annotate |