| Fri, 20 Dec 2019 10:24:52 +0100 |
ok again Test_Isac_Short since last 2 change sets
|
file | diff | annotate |
| Thu, 19 Dec 2019 17:37:25 +0100 |
lucin: unify fun.ids. for locate_input_tactic
|
file | diff | annotate |
| Thu, 19 Dec 2019 16:41:57 +0100 |
cleanup fun solve, shift from Solve --> Step_Solve
|
file | diff | annotate |
| Mon, 16 Dec 2019 14:03:16 +0100 |
lucin: re-build determine_next_tactic, "ONE ERROR" outcommented
|
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 |
| Tue, 19 Nov 2019 16:16:26 +0100 |
tuned
|
file | diff | annotate |
| Tue, 19 Nov 2019 16:12:25 +0100 |
[Test_Isac] lucin: revise Pstate {or, ...}, see TODO.thy
|
file | diff | annotate |
| Wed, 13 Nov 2019 12:06:40 +0100 |
lucin: suppose determine_next_tactic unnecessary in solve Apply_Method'
|
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 |
| Wed, 30 Oct 2019 11:02:41 +0100 |
lucin: extend istate with rule-set vor evaluation
|
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, 16 Oct 2019 13:37:48 +0200 |
lucin: NEW locate_input_tactic works
|
file | diff | annotate |
| Thu, 10 Oct 2019 19:54:51 +0200 |
[Test_Isac] NEW locate_input_tactic works except 3 tests in Knowledge/polyminus.sml
|
file | diff | annotate |
| Wed, 02 Oct 2019 15:14:51 +0200 |
lucin: generalise bound variable in Prog_Tac.Rewrite*Inst
|
file | diff | annotate |
| Tue, 01 Oct 2019 10:47:25 +0200 |
lucin: drop unused bool argument in tactic Rewrite*Inst
|
file | diff | annotate |
| Sun, 22 Sep 2019 16:52:14 +0200 |
adopt new files of ProgLang in test/..
|
file | diff | annotate |
| Wed, 18 Sep 2019 16:28:49 +0200 |
tests run in Test_Isac with ML_system_64 = "true"
|
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 |
| Tue, 17 Sep 2019 09:01:03 +0200 |
tuned
|
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 |
| Thu, 12 Sep 2019 14:42:53 +0200 |
/----- finish update Isabelle2018 --> Isabelle2019 for Test_Isac.thy
|
file | diff | annotate |
| Wed, 11 Sep 2019 18:02:35 +0200 |
Isabelle2018->19: rm libisabelle -- retain max.of interface
|
file | diff | annotate |
| Tue, 03 Sep 2019 12:40:27 +0200 |
lucin: reorganise theories in ProgLang
|
file | diff | annotate |
| Thu, 29 Aug 2019 10:59:57 +0200 |
separate Prog_Tac.thy
|
file | diff | annotate |
| Wed, 28 Aug 2019 11:21:26 +0200 |
reorganised MathEngine/ BridgeLibisabelle/
|
file | diff | annotate |
| Tue, 27 Aug 2019 15:31:45 +0200 |
[-Test_Isac ONLY biegelinie-1.sml] assign Input_Descript to Specify/-phase
|
file | diff | annotate |
| Tue, 27 Aug 2019 11:59:48 +0200 |
separate Specify/ from Interpret/
|
file | diff | annotate |
| Sat, 24 Aug 2019 12:59:39 +0200 |
now Test_Isac works (the last 2 changesets do NOT)
|
file | diff | annotate |
| Thu, 22 Aug 2019 16:48:04 +0200 |
lucin: rename Script --> Program
|
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 |
| Fri, 26 Jul 2019 16:34:41 +0200 |
lucin: prep. test for further improving sig. for locate_input_tactic
|
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 |
| Wed, 24 Jul 2019 09:32:17 +0200 |
lucin: improve signature of "fun locate_input_tactic"
|
file | diff | annotate |
| Thu, 04 Jul 2019 15:13:30 +0200 |
lucin: tuned
|
file | diff | annotate |
| Tue, 25 Jun 2019 16:21:18 +0200 |
lucin: adapt tests to new file src/../lucas-interpreter.sml
|
file | diff | annotate |
| Mon, 24 Jun 2019 15:53:50 +0200 |
repair Test_Isac for previous change set
|
file | diff | annotate |
| Sun, 23 Jun 2019 14:44:00 +0200 |
introduce Test_Isac_Short.thy
|
file | diff | annotate |