| Wed, 08 Apr 2020 16:56:47 +0200 |
separate struct Rewrite_Ord
|
file | diff | annotate |
| Wed, 08 Apr 2020 14:24:38 +0200 |
separate struct ThyC
|
file | diff | annotate |
| Wed, 08 Apr 2020 12:32:51 +0200 |
use new struct "Rule_Set" for renaming identifiers
|
file | diff | annotate |
| Mon, 06 Apr 2020 11:44:36 +0200 |
use "Rule_Set" for shorter identifiers
|
file | diff | annotate |
| Sat, 04 Apr 2020 12:11:32 +0200 |
separate Rule_Set from Rule
|
file | diff | annotate |
| Wed, 01 Apr 2020 18:54:03 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Wed, 01 Apr 2020 12:42:39 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Tue, 31 Mar 2020 15:43:33 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Thu, 20 Feb 2020 18:47:55 +0100 |
cleanup Tactic and prep.shift after Ctree
|
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 |
| Mon, 20 Jan 2020 11:48:59 +0100 |
postpone separation of Tactic
|
file | diff | annotate |
| Fri, 17 Jan 2020 13:14:11 +0100 |
lucin: introduce Calc.T and Program.T
|
file | diff | annotate |
| Thu, 19 Dec 2019 16:41:57 +0100 |
cleanup fun solve, shift from Solve --> Step_Solve
|
file | diff | annotate |
| Tue, 17 Dec 2019 17:52:48 +0100 |
revert previous changeset, see TODO.thy
|
file | diff | annotate |
| Tue, 17 Dec 2019 17:19:34 +0100 |
shift tactic.sml after ctree.sml, leave tactic-def.sml before
|
file | diff | annotate |
| Tue, 17 Dec 2019 16:31:46 +0100 |
lucin: shift Istate into Interpret/ from MathEngBasic
|
file | diff | annotate |
| Mon, 16 Dec 2019 15:56:20 +0100 |
rollback
|
file | diff | annotate |
| Mon, 16 Dec 2019 15:38:13 +0100 |
shift datatype appl: Chead --> Applicable
|
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 |
| Sat, 16 Nov 2019 17:13:52 +0100 |
lucin: consolidate Tactic, 1st
|
file | diff | annotate |
| Thu, 14 Nov 2019 12:08:05 +0100 |
tuned
|
file | diff | annotate |
| Thu, 14 Nov 2019 12:00:13 +0100 |
tuned
|
file | diff | annotate |
| Thu, 31 Oct 2019 13:48:06 +0100 |
tuned
|
file | diff | annotate |
| Thu, 31 Oct 2019 10:41:42 +0100 |
lucin: extend Pstate with an additional flag
|
file | diff | annotate |
| Sat, 26 Oct 2019 13:03:16 +0200 |
separate common base for Specify and Interpret
|
file | diff | annotate | base |