| Mon, 23 Mar 2020 13:31:29 +0100 |
separate structure Detail_Step
|
file | diff | annotate |
| Mon, 24 Feb 2020 17:51:26 +0100 |
prep.: add test-code and test, cleanup
|
file | diff | annotate |
| Sun, 09 Feb 2020 16:55:41 +0100 |
cleanup TODO
|
file | diff | annotate |
| Sat, 08 Feb 2020 12:41:27 +0100 |
LI: prep. test to re-build locate_input_term
|
file | diff | annotate |
| Mon, 20 Jan 2020 14:38:46 +0100 |
determine structure for TODO.thy
|
file | diff | annotate |
| Mon, 20 Jan 2020 11:11:56 +0100 |
lucin: cleanup Istate (doubled code in Istate_Def)
|
file | diff | annotate |
| Fri, 17 Jan 2020 13:14:11 +0100 |
lucin: introduce Calc.T and Program.T
|
file | diff | annotate |
| Wed, 06 Nov 2019 18:34:29 +0100 |
lucin: renaming for paper
|
file | diff | annotate |
| Sat, 26 Oct 2019 13:03:16 +0200 |
separate common base for Specify and Interpret
|
file | diff | annotate |
| Wed, 02 Oct 2019 16:02:17 +0200 |
lucin: use #> in Program in analogy to #> in Isabelle/ML
|
file | diff | annotate |
| Thu, 26 Sep 2019 17:47:10 +0200 |
adaptations for paper lucin-isa.tex
|
file | diff | annotate |
| Sun, 22 Sep 2019 16:52:14 +0200 |
adopt new files of ProgLang in test/..
|
file | diff | annotate |
| Sun, 22 Sep 2019 15:15:37 +0200 |
lucin: update comments on structure of import's and ML_file's
|
file | diff | annotate |
| Tue, 10 Sep 2019 17:15:41 +0200 |
Isabelle2018->19: unclarified "Exception- Size raised" in Build_Thydata.thy
|
file | diff | annotate |
| Tue, 10 Sep 2019 16:13:28 +0200 |
Isabelle2018->19: rm libisabelle finished, retain interface.sml
|
file | diff | annotate |
| Tue, 10 Sep 2019 10:47:18 +0200 |
Isabelle2018->19: rm libisabelle, not available for Isabelle2019
|
file | diff | annotate |
| Tue, 03 Sep 2019 12:40:27 +0200 |
lucin: reorganise theories in ProgLang
|
file | diff | annotate |
| Thu, 29 Aug 2019 10:59:57 +0200 |
separate Prog_Tac.thy
|
file | diff | annotate |
| Wed, 28 Aug 2019 11:21:26 +0200 |
reorganised MathEngine/ BridgeLibisabelle/
|
file | diff | annotate |
| Tue, 27 Aug 2019 15:31:45 +0200 |
[-Test_Isac ONLY biegelinie-1.sml] assign Input_Descript to Specify/-phase
|
file | diff | annotate |
| Mon, 26 Aug 2019 17:40:27 +0200 |
rename Isac.thy --> Isac_Knowledge.thy
|
file | diff | annotate |
| Fri, 23 Aug 2019 17:23:25 +0200 |
remove Delete.thy
|
file | diff | annotate |
| Fri, 23 Aug 2019 16:36:47 +0200 |
collect all defitions for both, ProgLang/ & Interpret/
|
file | diff | annotate |
| Thu, 22 Aug 2019 16:48:04 +0200 |
lucin: rename Script --> Program
|
file | diff | annotate |
| Fri, 09 Aug 2019 14:04:13 +0200 |
separater structure ContextC
|
file | diff | annotate |
| Thu, 11 Jul 2019 16:39:46 +0200 |
add update for istate, ctxt to Ctree
|
file | diff | annotate |
| Wed, 03 Jul 2019 15:09:16 +0200 |
lucin: fix Test_Isac, rename aux-funs in lucas-interpreter.
|
file | diff | annotate |
| Mon, 31 Dec 2018 14:49:16 +0100 |
[-Test_Isac] add an overlooked structure
|
file | diff | annotate |
| Fri, 14 Dec 2018 19:12:30 +0100 |
[-Test_Isac] funpack: prep.no.3 replace ID::type by char string
|
file | diff | annotate |
| Wed, 21 Nov 2018 12:32:54 +0100 |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
file | diff | annotate |
| Wed, 05 Sep 2018 15:34:39 +0200 |
Isabelle2017->18: use libisabelle as separate session
|
file | diff | annotate |
| Tue, 04 Sep 2018 14:50:30 +0200 |
Isabelle2017->18: add libisabelle, PROBLEM with session management:
|
file | diff | annotate |
| Thu, 23 Aug 2018 17:23:11 +0200 |
/----- finish update Isabelle2017 --> Isabelle2018
|
file | diff | annotate |
| Thu, 23 Aug 2018 09:42:19 +0200 |
Isabelle2017->18: Pure and HOL build with updated thm.ML
|
file | diff | annotate |
| Thu, 15 Mar 2018 12:42:04 +0100 |
separate structure Celem: CALC_ELEMENT, finished on src/
|
file | diff | annotate |
| Fri, 02 Mar 2018 14:19:59 +0100 |
separate structure TermC : TERMC
|
file | diff | annotate |
| Sun, 25 Feb 2018 16:31:17 +0100 |
Calc: cleanup test file
|
file | diff | annotate |
| Sun, 25 Feb 2018 12:36:23 +0100 |
separate structure Calc : NUMERAL_CALCULATION
|
file | diff | annotate |
| Sun, 25 Feb 2018 07:13:47 +0100 |
Rewrite: test on "exception TERM" in Build_Isac repaired
|
file | diff | annotate |
| Sat, 24 Feb 2018 16:09:24 +0100 |
Rewrite is broken; intermediate state for repair
|
file | diff | annotate |
| Sat, 24 Feb 2018 11:14:56 +0100 |
Rewrite: cleanup source file
|
file | diff | annotate |
| Wed, 14 Feb 2018 12:20:35 +0100 |
separate structure LTools : LANGUAGE_TOOLS
|
file | diff | annotate |
| Tue, 06 Feb 2018 15:26:05 +0100 |
Isabelle2015->17: Build_Isac works again
|
file | diff | annotate |
| Tue, 06 Feb 2018 15:20:52 +0100 |
Isabelle2015->17: theory formad changed
|
file | diff | annotate |
| Wed, 30 Nov 2016 12:09:24 +0100 |
added structure Rtools : REWRITE_TOOLS
|
file | diff | annotate |
| Thu, 24 Nov 2016 14:33:42 +0100 |
added structure Inform : INPUT_FORMULAS
|
file | diff | annotate |
| Tue, 22 Nov 2016 10:42:21 +0100 |
added structure Math_Engine : MATH_ENGINE
|
file | diff | annotate |
| Thu, 17 Nov 2016 16:40:27 +0100 |
close structures again after Test_Isac
|
file | diff | annotate |
| Wed, 13 Jan 2016 14:37:27 +0100 |
cleanup theory imports, part 1
|
file | diff | annotate |
| Thu, 17 Dec 2015 15:46:49 +0100 |
Build_Isac works with Isabelle2015, excludes Protocol.thy
|
file | diff | annotate |
| Mon, 07 Dec 2015 09:52:54 +0100 |
documented structure for inital imports
|
file | diff | annotate |
| Sat, 05 Dec 2015 14:26:29 +0100 |
before start update Isabelle2014 --> Isabelle2015
|
file | diff | annotate |
| Fri, 07 Aug 2015 15:52:17 +0200 |
PIDE: improved error-msg during embedding into Java-side
|
file | diff | annotate |
| Sat, 18 Jul 2015 15:37:40 +0200 |
PIDE: Mini_Test step 1 via math-engine corrected
|
file | diff | annotate |
| Sat, 18 Jul 2015 15:27:35 +0200 |
PIDE: Protocol imports isac/Knowledge
|
file | diff | annotate |
| Thu, 25 Jun 2015 11:39:47 +0200 |
PIDE: libisabelle embedded on ML-side
|
file | diff | annotate |
| Tue, 09 Jun 2015 09:37:29 +0200 |
PIDE: import libisabelle/../Protocol.thy and rename Interface --> Math_Engine
|
file | diff | annotate |
| Tue, 14 Apr 2015 14:36:02 +0200 |
print_depth to be replaced by configuration option "ML_print_depth"
|
file | diff | annotate |
| Mon, 28 Jul 2014 17:06:16 +0200 |
ad (a): thehier does not contain sym_thmID theorems anymore
|
file | diff | annotate |
| Sun, 22 Jun 2014 15:17:07 +0200 |
ad thehier: removed last two Unsychronized.ref
|
file | diff | annotate |