Fri, 22 Jan 2016 15:53:13 +0100 |
Walther Neuper |
update to libisabelle-0.2.2/../Protocol
|
changeset |
files
|
Thu, 21 Jan 2016 17:29:33 +0100 |
Walther Neuper |
an interesting ML_command
|
changeset |
files
|
Fri, 15 Jan 2016 09:35:24 +0100 |
Walther Neuper |
session for libisabelle + Isac
|
changeset |
files
|
Wed, 13 Jan 2016 14:37:27 +0100 |
Walther Neuper |
cleanup theory imports, part 1
|
changeset |
files
|
Wed, 13 Jan 2016 13:55:56 +0100 |
Walther Neuper |
made Knowledge independent from libraries
|
changeset |
files
|
Tue, 12 Jan 2016 19:52:36 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
Tue, 12 Jan 2016 19:52:22 +0100 |
Walther Neuper |
replace call of MutabelleExtra.thms_of
|
changeset |
files
|
Tue, 12 Jan 2016 19:47:59 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
Tue, 12 Jan 2016 14:40:55 +0100 |
Walther Neuper |
trials on physical and technical units
|
changeset |
files
|
Tue, 05 Jan 2016 11:40:04 +0100 |
Walther Neuper |
experiments with ROOT/paths for libisabelle-protocol
|
changeset |
files
|
Tue, 05 Jan 2016 11:13:20 +0100 |
Walther Neuper |
experiments with ROOT/paths in libisabelle-procol
|
changeset |
files
|
Mon, 04 Jan 2016 13:10:23 +0100 |
Walther Neuper |
libisabelle/Protocol: all subsequent operation_setup compile without error
|
changeset |
files
|
Mon, 04 Jan 2016 12:32:01 +0100 |
Walther Neuper |
libisabelle/Protocol: 1st operation_setup compiles without error
|
changeset |
files
|
Mon, 21 Dec 2015 14:19:03 +0100 |
Walther Neuper |
Isabelle2014-->15: Test_Isac is perfect
|
changeset |
files
|
Mon, 21 Dec 2015 14:06:19 +0100 |
Walther Neuper |
Isabelle2014-->15: finished closed Thm.thy for tests
|
changeset |
files
|
Mon, 21 Dec 2015 13:58:02 +0100 |
Walther Neuper |
Isabelle2014-->2015: dropped tests not required any more
|
changeset |
files
|
Mon, 21 Dec 2015 13:35:41 +0100 |
Walther Neuper |
built session Isac without libisabelle Protocol
|
changeset |
files
|
Thu, 17 Dec 2015 15:48:13 +0100 |
Walther Neuper |
added libisabelle-protocol
|
changeset |
files
|
Thu, 17 Dec 2015 15:46:49 +0100 |
Walther Neuper |
Build_Isac works with Isabelle2015, excludes Protocol.thy
|
changeset |
files
|
Mon, 07 Dec 2015 16:07:24 +0100 |
Walther Neuper |
Isabelle2014-->15: removed errors from d9c3e373f8f5
|
changeset |
files
|
Mon, 07 Dec 2015 15:37:09 +0100 |
Walther Neuper |
Isabelle2015 NEWS: "^^^" handles negative numerals differently
|
changeset |
files
|
Mon, 07 Dec 2015 14:10:59 +0100 |
Walther Neuper |
Isabelle2014-->15: closed Thm.thy applied to tests
|
changeset |
files
|
Mon, 07 Dec 2015 11:32:12 +0100 |
Walther Neuper |
Isabelle2014-->15: rem_thm-->Thm.rep_thm
|
changeset |
files
|
Mon, 07 Dec 2015 11:25:02 +0100 |
Walther Neuper |
Isabelle2014-->15: term_of-->Thm.term_of
|
changeset |
files
|
Mon, 07 Dec 2015 10:52:07 +0100 |
Walther Neuper |
Isabelle2014-->15: Thm.thy is not open anymore, further funs qualified
|
changeset |
files
|
Mon, 07 Dec 2015 10:17:08 +0100 |
Walther Neuper |
sabelle2014-->15: cterm_of-->Thm.global_cterm_of
|
changeset |
files
|
Mon, 07 Dec 2015 10:01:49 +0100 |
Walther Neuper |
Isabelle2014-->15: prop_of-->Thm.prop_of
|
changeset |
files
|
Mon, 07 Dec 2015 09:52:54 +0100 |
Walther Neuper |
documented structure for inital imports
|
changeset |
files
|
Sun, 06 Dec 2015 08:45:16 +0100 |
Walther Neuper |
merged Isac's hooks into Isabelle
|
changeset |
files
|
Sat, 05 Dec 2015 16:09:41 +0100 |
Walther Neuper |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
changeset |
files
|
Sat, 05 Dec 2015 14:26:56 +0100 |
Walther Neuper |
Added tag Isabelle2014/Isac for changeset d61d51765a02
|
changeset |
files
|
Sat, 05 Dec 2015 14:26:29 +0100 |
Walther Neuper |
before start update Isabelle2014 --> Isabelle2015
Isabelle2014/Isac
|
changeset |
files
|
Tue, 06 Oct 2015 15:56:47 +0200 |
Walther Neuper |
PIDE: corrected PIDE's strange handling of strings
|
changeset |
files
|
Tue, 06 Oct 2015 15:51:10 +0200 |
Walther Neuper |
PIDE: (Knowledge-)Context works also for met FINALLY
|
changeset |
files
|
Tue, 06 Oct 2015 09:34:43 +0200 |
Walther Neuper |
PIDE: (Knowledge-)Context works also for met
|
changeset |
files
|
Sun, 20 Sep 2015 16:04:35 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Sun, 20 Sep 2015 13:17:37 +0200 |
Walther Neuper |
found a failing test without assertion; check XML ?
|
changeset |
files
|
Sun, 20 Sep 2015 11:29:49 +0200 |
Walther Neuper |
unified (Knowledge-)Context for thy, pbl, met
|
changeset |
files
|
Sun, 13 Sep 2015 12:37:57 +0200 |
Walther Neuper |
improved exception handling in XML conversion
|
changeset |
files
|
Sun, 13 Sep 2015 12:25:30 +0200 |
Walther Neuper |
updated tests to changes in 636013c7949f
|
changeset |
files
|
Sat, 29 Aug 2015 08:35:26 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Sat, 29 Aug 2015 08:33:54 +0200 |
Walther Neuper |
PIDE-phase 2c CONTINUED: IsaToJava.fetch_proposed_tac_out failed due to wrong XML conversion on SML-side
|
changeset |
files
|
Tue, 25 Aug 2015 06:13:07 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Tue, 25 Aug 2015 06:04:18 +0200 |
Walther Neuper |
PIDE: note on state of interface.sml -- isac-java
|
changeset |
files
|
Mon, 24 Aug 2015 10:21:14 +0200 |
Walther Neuper |
PIDE-phase 2c CONTINUED: removed error in Protocol
|
changeset |
files
|
Thu, 20 Aug 2015 16:18:36 +0200 |
Walther Neuper |
PIDE-phase 2c: Protocol changed to make IsaToJava simpler
|
changeset |
files
|
Tue, 18 Aug 2015 17:39:47 +0200 |
Walther Neuper |
PIDE-phase 2c: Protocol is stable with minimal changes
|
changeset |
files
|
Sat, 15 Aug 2015 16:03:53 +0200 |
Walther Neuper |
PIDE-phase-2a: changed XML for Tactic, driven from isac-java
|
changeset |
files
|
Sat, 15 Aug 2015 08:55:27 +0200 |
Walther Neuper |
PIDE-phase-2a: cleaned xml_of_tac
|
changeset |
files
|
Sat, 15 Aug 2015 08:06:28 +0200 |
Walther Neuper |
PIDE-phase-2a: xml_of_tac reordered
|
changeset |
files
|
Fri, 14 Aug 2015 17:25:55 +0200 |
Walther Neuper |
PIDE-phase-2a: xml_of_tac: different substitutions converted to same XML
|
changeset |
files
|
Fri, 14 Aug 2015 10:01:33 +0200 |
Walther Neuper |
PIDE-phase-2a: corrected XML conversion for Tactics
|
changeset |
files
|
Thu, 13 Aug 2015 10:46:31 +0200 |
Walther Neuper |
PIDE-phase-2a: corrected XML conversion for intree of appendFormula
|
changeset |
files
|
Tue, 11 Aug 2015 15:39:27 +0200 |
Walther Neuper |
PIDE-phase-2a: xml_to_* for operation_setup of all Math_Engine
|
changeset |
files
|
Sun, 09 Aug 2015 17:52:02 +0200 |
Walther Neuper |
PIDE: auxiliary funs for operation_setup apply_tac
|
changeset |
files
|
Sun, 09 Aug 2015 15:15:01 +0200 |
Walther Neuper |
PIDE: auxiliary funs for operation_setup append_form
|
changeset |
files
|
Sun, 09 Aug 2015 10:00:11 +0200 |
Walther Neuper |
PIDE: reorder structure Math_Engine for implementation of interface in libisabelle
|
changeset |
files
|
Fri, 07 Aug 2015 15:52:17 +0200 |
Walther Neuper |
PIDE: improved error-msg during embedding into Java-side
|
changeset |
files
|
Fri, 24 Jul 2015 08:09:06 +0200 |
Walther Neuper |
PIDE: corrected XML generation
|
changeset |
files
|
Fri, 24 Jul 2015 07:47:06 +0200 |
Walther Neuper |
PIDE: added missing code in interface-xml
|
changeset |
files
|