| Wed, 30 Oct 2019 11:02:41 +0100 |
Walther Neuper |
lucin: extend istate with rule-set vor evaluation
|
changeset |
files
|
| Sun, 27 Oct 2019 12:10:57 +0100 |
Walther Neuper |
lucin: replace Istate.safe by Istate.appy_
|
changeset |
files
|
| Sat, 26 Oct 2019 13:03:16 +0200 |
Walther Neuper |
separate common base for Specify and Interpret
|
changeset |
files
|
| Fri, 25 Oct 2019 16:07:15 +0200 |
Walther Neuper |
lucin: adopt Poly/ML warnings in lucas-interpreter.sml
|
changeset |
files
|
| Fri, 25 Oct 2019 15:06:08 +0200 |
Walther Neuper |
lucin: remove old args in appy & Co
|
changeset |
files
|
| Fri, 25 Oct 2019 10:11:55 +0200 |
Walther Neuper |
lucin: appy & Co with istate + old args works
|
changeset |
files
|
| Tue, 22 Oct 2019 17:35:50 +0200 |
Walther Neuper |
lucin: prep. tests for appy & Co with interpretere-state
|
changeset |
files
|
| Sat, 19 Oct 2019 18:19:16 +0200 |
Walther Neuper |
lucin: introduce interpreter-state to appy & Co
|
changeset |
files
|
| Sat, 19 Oct 2019 17:18:44 +0200 |
Walther Neuper |
lucin: cleanup args in lucas-interpreter, ass_up works
|
changeset |
files
|
| Sat, 19 Oct 2019 15:05:02 +0200 |
Walther Neuper |
renaming
|
changeset |
files
|
| Sat, 19 Oct 2019 14:59:09 +0200 |
Walther Neuper |
lucin: assimilate signatures
|
changeset |
files
|
| Sat, 19 Oct 2019 14:26:58 +0200 |
Walther Neuper |
lucin: correct an error, undetected by Test_Isac(!)
|
changeset |
files
|
| Sat, 19 Oct 2019 14:07:27 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 19 Oct 2019 11:22:26 +0200 |
Walther Neuper |
lucin: cleanup args in lucas-interpreter, ass_up prep.
|
changeset |
files
|
| Sat, 19 Oct 2019 11:01:11 +0200 |
Walther Neuper |
lucin: cleanup args in lucas-interpreter, assy works
|
changeset |
files
|
| Fri, 18 Oct 2019 17:00:36 +0200 |
Walther Neuper |
lucin: cleanup args in lucas-interpreter, new assy with errors outcommented
|
changeset |
files
|
| Fri, 18 Oct 2019 16:18:14 +0200 |
Walther Neuper |
lucin: cleanup args in lucas-interpreter, preps 2
|
changeset |
files
|
| Thu, 17 Oct 2019 13:17:48 +0200 |
Walther Neuper |
lucin: cleanup args in lucas-interpreter, preps
|
changeset |
files
|
| Wed, 16 Oct 2019 17:24:26 +0200 |
Walther Neuper |
lucin: cleanup locate_input_tactic
|
changeset |
files
|
| Wed, 16 Oct 2019 16:20:21 +0200 |
Walther Neuper |
lucin: cleanup return values of locate_input_tactic
|
changeset |
files
|
| Wed, 16 Oct 2019 13:37:48 +0200 |
Walther Neuper |
lucin: NEW locate_input_tactic works
|
changeset |
files
|
| Thu, 10 Oct 2019 19:54:51 +0200 |
Walther Neuper |
[Test_Isac] NEW locate_input_tactic works except 3 tests in Knowledge/polyminus.sml
|
changeset |
files
|
| Wed, 09 Oct 2019 12:28:46 +0200 |
Walther Neuper |
[Test_Isac] NEW locate_input_tactic works in Test_Some
|
changeset |
files
|
| Tue, 08 Oct 2019 15:32:42 +0200 |
Walther Neuper |
[Test_Isac] cp NEW locate_input_tactic from Test_Some to src ..
|
changeset |
files
|
| Mon, 07 Oct 2019 17:50:26 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 07 Oct 2019 17:21:47 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 07 Oct 2019 13:52:36 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 07 Oct 2019 12:53:08 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 07 Oct 2019 11:11:32 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 16:33:25 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 16:18:33 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 16:15:38 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 16:02:14 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 15:48:41 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 15:46:30 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 14:51:46 +0200 |
Walther Neuper |
lucin: clarify signature for locate_input_tactic, prep.
|
changeset |
files
|
| Sat, 05 Oct 2019 13:46:21 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 05 Oct 2019 11:47:02 +0200 |
Walther Neuper |
lucin: clarify signature for locate_input_tactic, prep.
|
changeset |
files
|
| Fri, 04 Oct 2019 13:27:15 +0200 |
Walther Neuper |
lucin: taci list NEVER WITH length > 1 FROM locate_input_tac
|
changeset |
files
|
| Wed, 02 Oct 2019 16:02:17 +0200 |
Walther Neuper |
lucin: use #> in Program in analogy to #> in Isabelle/ML
|
changeset |
files
|
| Wed, 02 Oct 2019 15:14:51 +0200 |
Walther Neuper |
lucin: generalise bound variable in Prog_Tac.Rewrite*Inst
|
changeset |
files
|
| Tue, 01 Oct 2019 10:47:25 +0200 |
Walther Neuper |
lucin: drop unused bool argument in tactic Rewrite*Inst
|
changeset |
files
|
| Thu, 26 Sep 2019 17:47:10 +0200 |
Walther Neuper |
adaptations for paper lucin-isa.tex
|
changeset |
files
|
| Sun, 22 Sep 2019 16:52:14 +0200 |
Walther Neuper |
adopt new files of ProgLang in test/..
|
changeset |
files
|
| Sun, 22 Sep 2019 15:15:37 +0200 |
Walther Neuper |
lucin: update comments on structure of import's and ML_file's
|
changeset |
files
|
| Sun, 22 Sep 2019 14:51:29 +0200 |
Walther Neuper |
remove updates for test-mode, i.e. an accident from previous changeset
|
changeset |
files
|
| Sun, 22 Sep 2019 14:47:35 +0200 |
Walther Neuper |
lucin: shift ListC.thy into ProgLang
|
changeset |
files
|
| Wed, 18 Sep 2019 17:23:02 +0200 |
Walther Neuper |
return to default mode
|
changeset |
files
|
| Wed, 18 Sep 2019 16:28:49 +0200 |
Walther Neuper |
tests run in Test_Isac with ML_system_64 = "true"
|
changeset |
files
|
| Wed, 18 Sep 2019 12:15:59 +0200 |
Walther Neuper |
tests run in Test_Isac with ML_system_64 = "true", still exception Size
|
changeset |
files
|
| Tue, 17 Sep 2019 10:25:24 +0200 |
Walther Neuper |
tests run in Text_Isac_Short.thy in x86_64_32 mode of Poly/ML 5.8
|
changeset |
files
|
| Tue, 17 Sep 2019 09:01:57 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Tue, 17 Sep 2019 09:01:03 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 16 Sep 2019 20:40:33 +0200 |
Walther Neuper |
[Test_Isac] notes and out-commenting in tests
|
changeset |
files
|
| Mon, 16 Sep 2019 19:39:48 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 16 Sep 2019 13:47:30 +0200 |
Walther Neuper |
Build_Isac.thy , isabelle build and Test_Isac_Short.thy in x86_64_32 mode
|
changeset |
files
|
| Mon, 16 Sep 2019 12:43:43 +0200 |
Walther Neuper |
shift respective constants to ListC.thy
|
changeset |
files
|
| Sat, 14 Sep 2019 16:15:05 +0200 |
Walther Neuper |
lucin: cleanup and comment thys in ProgLang
|
changeset |
files
|
| Fri, 13 Sep 2019 18:35:51 +0200 |
Walther Neuper |
lucin: cleanup thys in ProgLang, in particular Aut_Prog.thy
|
changeset |
files
|
| Thu, 12 Sep 2019 14:42:53 +0200 |
Walther Neuper |
/----- finish update Isabelle2018 --> Isabelle2019 for Test_Isac.thy
|
changeset |
files
|