| Tue, 04 Feb 2020 17:11:54 +0100 |
lucin: rename central structure to Lucin
|
file | diff | annotate |
| Tue, 04 Feb 2020 16:45:36 +0100 |
lucin: clarify path handling
|
file | diff | annotate |
| Tue, 04 Feb 2020 16:27:54 +0100 |
lucin: set_found ONCE in locate_input_tactic makes "fun me" work
|
file | diff | annotate |
| Sat, 25 Jan 2020 12:45:51 +0100 |
tuned
|
file | diff | annotate |
| Thu, 23 Jan 2020 11:12:09 +0100 |
repair last changeset, rename set_skip -> set_found (according last change)
|
file | diff | annotate |
| Thu, 23 Jan 2020 10:48:57 +0100 |
lucin: renaming due to simpler scanning (Istate .. found_accept)
|
file | diff | annotate |
| Wed, 22 Jan 2020 17:32:45 +0100 |
lucin: simpler Lucin.scan_up works, but ERROR "LI.find_next_step without result" outcommented
|
file | diff | annotate |
| Wed, 22 Jan 2020 11:44:56 +0100 |
lucin: Accept_Tac sets to Skip_ (later: found = true) instead of AppUndef_ (later false)
|
file | diff | annotate |
| Tue, 21 Jan 2020 09:09:11 +0100 |
lucin: towards simplifying Lucin.scan*
|
file | diff | annotate |
| Mon, 20 Jan 2020 14:38:46 +0100 |
determine structure for TODO.thy
|
file | diff | annotate |
| Sun, 19 Jan 2020 16:38:07 +0100 |
tuned
|
file | diff | annotate |
| Fri, 17 Jan 2020 14:10:10 +0100 |
tuned
|
file | diff | annotate |
| Fri, 17 Jan 2020 13:47:19 +0100 |
lucin: cleanup code
|
file | diff | annotate |
| Fri, 17 Jan 2020 13:14:11 +0100 |
lucin: introduce Calc.T and Program.T
|
file | diff | annotate |
| Fri, 17 Jan 2020 12:37:21 +0100 |
lucin: renaming
|
file | diff | annotate |
| Wed, 15 Jan 2020 13:50:16 +0100 |
lucin: rename completed
|
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 |
| Wed, 15 Jan 2020 12:01:13 +0100 |
tuned
|
file | diff | annotate |
| Wed, 15 Jan 2020 11:47:38 +0100 |
preps for IJCAR paper
|
file | diff | annotate |
| Mon, 23 Dec 2019 11:12:24 +0100 |
lucin: unify signatures of Step*
|
file | diff | annotate |
| Sat, 21 Dec 2019 16:45:10 +0100 |
lucin: unify do_next, partially
|
file | diff | annotate |
| Sat, 21 Dec 2019 16:07:18 +0100 |
lucin: unify Step_Solve.by_tactic -- Lucin(NEW).by_tactic, partially
|
file | diff | annotate |
| Sat, 21 Dec 2019 15:17:46 +0100 |
lucin: prep. unify Step_Solve.by_tactic -- Lucin(NEW).by_tactic
|
file | diff | annotate |
| Sat, 21 Dec 2019 13:34:02 +0100 |
shift appropriate funs to Pos.
|
file | diff | annotate |
| Sat, 21 Dec 2019 13:04:56 +0100 |
lucin: prep. unify Step_Solve.by_tactic -- Lucin(NEW).by_tactic
|
file | diff | annotate |
| Fri, 20 Dec 2019 09:57:45 +0100 |
cleanup code
|
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 |
| Thu, 19 Dec 2019 12:40:17 +0100 |
lucin: various investigations (a chaos change set)
|
file | diff | annotate |
| Wed, 18 Dec 2019 15:33:27 +0100 |
prep. intro. of Step
|
file | diff | annotate |
| Wed, 18 Dec 2019 14:48:43 +0100 |
cleanup, unify code for Check_Postcond'
|
file | diff | annotate |
| Wed, 18 Dec 2019 12:40:49 +0100 |
cleanup OLD NEW
|
file | diff | annotate |
| Wed, 18 Dec 2019 11:31:31 +0100 |
lucin: plan for new identifiers of steps
|
file | diff | annotate |
| Wed, 18 Dec 2019 11:02:32 +0100 |
hack until review of Specify
|
file | diff | annotate |
| Mon, 16 Dec 2019 15:38:13 +0100 |
shift datatype appl: Chead --> Applicable
|
file | diff | annotate |
| Mon, 16 Dec 2019 14:03:16 +0100 |
lucin: re-build determine_next_tactic, "ONE ERROR" outcommented
|
file | diff | annotate |
| Sat, 14 Dec 2019 13:36:40 +0100 |
remove tracing, which interfere with current investigations
|
file | diff | annotate |
| Sat, 14 Dec 2019 09:41:17 +0100 |
lucin: drop unnecessary call of determine_next_tactic
|
file | diff | annotate |
| Fri, 13 Dec 2019 15:56:10 +0100 |
lucin: prep.re-build of determine_next_tactic in Test_Some.thy: return values used
|
file | diff | annotate |
| Sat, 30 Nov 2019 17:03:49 +0100 |
lucin: code cleanup
|
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 17:19:37 +0100 |
lucin: test setup downto fun determine_next_tactic
|
file | diff | annotate |
| Fri, 29 Nov 2019 16:06:30 +0100 |
lucin: test setup for re-building fun determine_next_tactic
|
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, 26 Nov 2019 17:37:17 +0100 |
lucin: improve readability
|
file | diff | annotate |
| Tue, 26 Nov 2019 17:12:27 +0100 |
lucin: shift code for paper
|
file | diff | annotate |
| Tue, 26 Nov 2019 17:06:12 +0100 |
lucin: cleanup ContextC, partially
|
file | diff | annotate |
| Mon, 25 Nov 2019 16:39:52 +0100 |
lucin: renaming in scanning the parse-tree
|
file | diff | annotate |
| Thu, 21 Nov 2019 15:31:32 +0100 |
lucin: shift datatype, rename
|
file | diff | annotate |
| Thu, 21 Nov 2019 12:05:56 +0100 |
lucin: prep.to unitise handling of tactics
|
file | diff | annotate |
| Tue, 19 Nov 2019 16:18:16 +0100 |
tuned
|
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 |
| Tue, 19 Nov 2019 14:19:44 +0100 |
lucin: improve naming for constructors in scans
|
file | diff | annotate |
| Sat, 16 Nov 2019 20:38:55 +0100 |
lucin: simplify scan for determine_next_tactic according to 86f2102fd7a8
|
file | diff | annotate |
| Sat, 16 Nov 2019 20:13:43 +0100 |
tuned
|
file | diff | annotate |
| Sat, 16 Nov 2019 20:11:28 +0100 |
lucin: simplify scan for locate_input_tactic according to 86f2102fd7a8
|
file | diff | annotate |
| Sat, 16 Nov 2019 19:01:04 +0100 |
lucin: found returning Env.T unnecessary in Skip1,2 and Napp
|
file | diff | annotate |
| Sat, 16 Nov 2019 18:25:31 +0100 |
lucin: scanning with Skip1 need NOT return env
|
file | diff | annotate |