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 |
Thu, 19 Jun 2014 08:27:19 +0200 |
ad 967c8a1eb6b1 thehier: ATTENTION: some works only in session Isac, not in Build_Isac.thy
|
file | diff | annotate |
Thu, 19 Jun 2014 07:40:46 +0200 |
ad 967c8a1eb6b1 (2,6) thehier: final repair of KEStore_Elems.add_thes
|
file | diff | annotate |
Sun, 15 Jun 2014 18:39:59 +0200 |
merged
|
file | diff | annotate |
Sun, 15 Jun 2014 18:27:23 +0200 |
ad 967c8a1eb6b1 (2,3) thehier: ugly chunk makes Test_Isac run
|
file | diff | annotate |
Fri, 13 Jun 2014 12:59:29 +0200 |
tuned
|
file | diff | annotate |
Fri, 06 Jun 2014 06:51:58 +0200 |
survey on remaining Unsynchronized.ref
|
file | diff | annotate |
Thu, 05 Jun 2014 18:10:46 +0200 |
plans for approaching Isabelle with Isac
|
file | diff | annotate |
Thu, 21 Nov 2013 11:46:00 +0100 |
Isabelle2013 --> 2013-1: replace an Isabelle constant newly introduced
|
file | diff | annotate |
Wed, 17 Jul 2013 07:32:53 +0200 |
--- heap image for Isac on Isabelle2013 builds
|
file | diff | annotate |
Mon, 15 Jul 2013 08:28:50 +0200 |
--- Build_Isac.thy runs on Isabelle2013
|
file | diff | annotate |
Thu, 11 Jul 2013 16:58:31 +0200 |
end of improving tests for isac on Isabelle2012
|
file | diff | annotate |
Thu, 20 Jun 2013 17:53:47 +0200 |
manually completed "thehier" such that insert_errpats, insert_fillpats
|
file | diff | annotate |
Tue, 18 Jun 2013 08:19:57 +0200 |
Build_Isac.thy and creating Isac heap OK
|
file | diff | annotate |
Sun, 16 Jun 2013 12:31:41 +0200 |
Isabelle2011 --> 2012 intermediate
|
file | diff | annotate |
Sun, 14 Oct 2012 21:26:02 +0200 |
2011-->2012: "isabelle usedir -b HOL Isac" works
|
file | diff | annotate |
Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
file | diff | annotate |
Sun, 14 Oct 2012 14:43:41 +0200 |
2011-->2012: Script
|
file | diff | annotate |