| Tue, 20 Apr 2021 16:58:44 +0200 |
replace power ^^^ by \<up>
|
file | diff | annotate |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Mon, 29 Jun 2020 16:01:01 +0200 |
renamings for Isabelle WS
|
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 |
| Fri, 15 May 2020 11:46:43 +0200 |
shift code from Specification to appropriate locations
|
file | diff | annotate |
| Thu, 14 May 2020 16:58:33 +0200 |
shift code from P_Specific --> CAS_Cmd
|
file | diff | annotate |
| Thu, 14 May 2020 16:08:41 +0200 |
shift code Specification --> Calc
|
file | diff | annotate |
| Thu, 14 May 2020 15:06:18 +0200 |
Test_Isac_Short works with P_Specific
|
file | diff | annotate |
| Thu, 14 May 2020 14:49:13 +0200 |
analogous naming P_Specific .. P_Model
|
file | diff | annotate |
| Thu, 14 May 2020 13:48:45 +0200 |
rename to Specification, contiued
|
file | diff | annotate |
| Tue, 12 May 2020 17:42:29 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Mon, 04 May 2020 16:25:14 +0200 |
shift code specific for specify-phase to Specify/*
|
file | diff | annotate |
| Mon, 04 May 2020 09:25:51 +0200 |
separate Solve_Step.add, rearrange code, prep. Specify_Step
|
file | diff | annotate |
| Fri, 01 May 2020 16:06:59 +0200 |
separate Specify_Step.check
|
file | diff | annotate |
| Fri, 01 May 2020 15:28:40 +0200 |
separate Solve_Step.check, repair ALL of Test_Isac_Short
|
file | diff | annotate |
| Wed, 29 Apr 2020 12:30:51 +0200 |
prep. separation of check Applicable between specify-phase and solve-phase
|
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 18:00:58 +0200 |
collect code in ThyC
|
file | diff | annotate |
| Wed, 15 Apr 2020 11:37:43 +0200 |
cleanup
|
file | diff | annotate |
| Fri, 10 Apr 2020 18:32:36 +0200 |
use "UnparseC" for renaming identifiers
|
file | diff | annotate |
| Fri, 10 Apr 2020 14:46:55 +0200 |
rearrange code for ThmC
|
file | diff | annotate |
| Thu, 09 Apr 2020 18:21:09 +0200 |
rearrange code in Rule_Set and Rule
|
file | diff | annotate |
| Thu, 09 Apr 2020 17:13:17 +0200 |
separate struct. UnparseC, shift code to ThmC
|
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 |
| 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 |
| Wed, 01 Apr 2020 10:24:13 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Tue, 31 Mar 2020 15:43:33 +0200 |
renaming, cleanup
|
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 |
| Wed, 25 Mar 2020 10:38:31 +0100 |
remove unused field in Ctree
|
file | diff | annotate |
| Wed, 25 Mar 2020 09:38:40 +0100 |
cleanup LItool.resume_prog, cf.edf1643edde5
|
file | diff | annotate |
| Mon, 23 Mar 2020 14:55:34 +0100 |
start restructuring test/../isac/*
|
file | diff | annotate |
| Wed, 18 Mar 2020 15:23:15 +0100 |
prep. cleanup LItool.resume_prog
|
file | diff | annotate |
| Sat, 07 Mar 2020 17:11:55 +0100 |
cleanup LItool, begin
|
file | diff | annotate |
| Sat, 07 Mar 2020 15:37:37 +0100 |
further separate specify- and solve-phase
|
file | diff | annotate |
| Thu, 20 Feb 2020 18:02:00 +0100 |
prep. cleanup istate/ctxt in Ctree, part 4
|
file | diff | annotate |
| Thu, 20 Feb 2020 17:09:24 +0100 |
prep. cleanup istate/ctxt in Ctree, part 3
|
file | diff | annotate |
| Thu, 20 Feb 2020 14:57:03 +0100 |
prep. cleanup istate/ctxt in Ctree, part 2
|
file | diff | annotate |
| Thu, 20 Feb 2020 11:55:29 +0100 |
prep. cleanup istate/ctxt in Ctree
|
file | diff | annotate |
| Sun, 16 Feb 2020 16:26:05 +0100 |
introduce Step.by_tactic, part 3, finished, Test_Isac_Short OK
|
file | diff | annotate |
| Tue, 11 Feb 2020 11:58:45 +0100 |
introduce Step.by_tactic, part 1
|
file | diff | annotate |
| Mon, 10 Feb 2020 17:01:49 +0100 |
replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly
|
file | diff | annotate |
| Sun, 09 Feb 2020 12:48:18 +0100 |
cleanup TODOs
|
file | diff | annotate |
| Sat, 08 Feb 2020 17:00:37 +0100 |
replace Chead.calcstate' by Calc.T once
|
file | diff | annotate |
| Sat, 08 Feb 2020 16:33:27 +0100 |
step separated wrt Solve .. Specify
|
file | diff | annotate |
| Sat, 08 Feb 2020 14:44:24 +0100 |
LI: locat_input_term has signature as required
|
file | diff | annotate |
| Fri, 07 Feb 2020 13:03:11 +0100 |
LI: Test_Isac_Short OK also for test from last changeset
|
file | diff | annotate |
| Fri, 07 Feb 2020 12:56:02 +0100 |
LI: safe test for re-build fun find_next_step
|
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 |
| Tue, 04 Feb 2020 16:30:44 +0100 |
tuned
|
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 |
| 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:20:54 +0100 |
lucin: tests towards simpl. Lucin.scan*
|
file | diff | annotate |
| Mon, 20 Jan 2020 11:11:56 +0100 |
lucin: cleanup Istate (doubled code in Istate_Def)
|
file | diff | annotate |