| Mon, 22 Aug 2022 11:26:20 +0200 |
cleanup test for: push ctxt through LI
|
file | diff | annotate |
| Tue, 16 Aug 2022 15:53:20 +0200 |
prepare test 2 for: push ctxt through LI
|
file | diff | annotate |
| Mon, 19 Jul 2021 17:29:35 +0200 |
introduce ALL valid const_name in test/*
|
file | diff | annotate |
| Thu, 15 Jul 2021 14:10:18 +0200 |
ewrite.sml + poly.sml + rational.sml: ok, repair rewrite-orders
|
file | diff | annotate |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Wed, 03 Jun 2020 11:25:19 +0200 |
follow 2 ancient updates of Library.ML
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Tue, 28 Apr 2020 15:31:49 +0200 |
assign code from Rtools to appropriate struct.s
|
file | diff | annotate |
| Wed, 22 Apr 2020 14:36:27 +0200 |
use "Spec", "Problem", "Method" for renaming identifiers
|
file | diff | annotate |
| Tue, 21 Apr 2020 15:42:50 +0200 |
replace Celem. with new struct.s in BaseDefinitions/
|
file | diff | annotate |
| Wed, 15 Apr 2020 16:46:41 +0200 |
use "ThyC" for renaming identifiers finished, cleanup
|
file | diff | annotate |
| Fri, 10 Apr 2020 18:32:36 +0200 |
use "UnparseC" for renaming identifiers
|
file | diff | annotate |
| Thu, 09 Apr 2020 17:13:17 +0200 |
separate struct. UnparseC, shift code to ThmC
|
file | diff | annotate |
| Tue, 31 Mar 2020 14:05:10 +0200 |
remove assumptions from Check_Postcond'; these are done by context now
|
file | diff | annotate |
| Mon, 23 Mar 2020 17:51:35 +0100 |
make Check_elementwise' idle wrt. Calc.T
|
file | diff | annotate |
| Wed, 18 Mar 2020 15:23:15 +0100 |
prep. cleanup LItool.resume_prog
|
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 |
| 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 |
| Fri, 17 Jan 2020 13:47:19 +0100 |
lucin: cleanup code
|
file | diff | annotate |
| Fri, 17 Jan 2020 12:37:21 +0100 |
lucin: renaming
|
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 16:58:36 +0100 |
shift code from mathengine-stateless.sml to Step.do_next
|
file | diff | annotate |
| Mon, 23 Dec 2019 16:38:09 +0100 |
rm code replaced in previous change set
|
file | diff | annotate |
| Sat, 21 Dec 2019 18:05:13 +0100 |
lucin: unify do_next postponed
|
file | diff | annotate |
| Sat, 21 Dec 2019 16:45:10 +0100 |
lucin: unify do_next, partially
|
file | diff | annotate |
| Wed, 18 Dec 2019 11:31:31 +0100 |
lucin: plan for new identifiers of steps
|
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 |