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 |
Fri, 12 Oct 2012 17:06:58 +0200 |
2011-->2012: ProofContext-->Proof_Context
|
file | diff | annotate |
Fri, 12 Oct 2012 16:03:07 +0200 |
2011-->2012:
|
file | diff | annotate |
Fri, 04 May 2012 08:51:42 +0200 |
made 3 exps SignalProcessing run
|
file | diff | annotate |
Tue, 10 Apr 2012 09:31:21 +0200 |
xml-files created from Knowledge (Isabelle2002 --> 2011)
|
file | diff | annotate |
Thu, 05 Apr 2012 11:31:56 +0200 |
thydata created (Isabelle2002 --> 2011)
|
file | diff | annotate |
Wed, 23 Mar 2011 17:20:39 +0100 |
make Test_Isac.thy run in jEdit; intermed.
|
file | diff | annotate |
Thu, 17 Mar 2011 10:11:18 +0100 |
intermed. usecase Diophant
|
file | diff | annotate |
Thu, 03 Mar 2011 17:37:46 +0100 |
Update to Isabelle 2011: Build_Isac works now
|
file | diff | annotate |
Thu, 03 Mar 2011 16:38:59 +0100 |
intermed.update to Isabelle 2011
|
file | diff | annotate |
Tue, 01 Mar 2011 15:23:59 +0100 |
intermed.update to Isabelle2011: test/../syntax added
|
file | diff | annotate |
Sat, 26 Feb 2011 12:37:58 +0100 |
intermed.update to Isabelle2011: ProgLang works
|
file | diff | annotate |
Sat, 26 Feb 2011 11:34:08 +0100 |
intermed.update to Isabelle2011
|
file | diff | annotate |
Fri, 25 Feb 2011 13:26:45 +0100 |
buid Pur, HOL worked
|
file | diff | annotate |
Thu, 18 Nov 2010 17:46:22 +0100 |
reactivated by 'hg up -C isac-update-Isa09-2'
|
file | diff | annotate |
Fri, 29 Oct 2010 15:54:16 +0200 |
trials on scala with inssort
|
file | diff | annotate |
Mon, 11 Oct 2010 12:55:40 +0200 |
intermed. repair Isac.thy, thehier := the_hier ...
|
file | diff | annotate |
Fri, 08 Oct 2010 18:51:23 +0200 |
repaired fun nxt_specify_
|
file | diff | annotate |
Tue, 28 Sep 2010 07:28:10 +0200 |
repaired fun uminus_to_string, fun rewrite_terms_
|
file | diff | annotate |
Thu, 23 Sep 2010 16:38:25 +0200 |
changed 'writeln' --> 'tracing' in src/ and _NOT_ in test/
|
file | diff | annotate |
Thu, 23 Sep 2010 08:43:36 +0200 |
repaired is_copy_named, cpy_nam and improved tests & comments
|
file | diff | annotate |
Tue, 14 Sep 2010 15:46:56 +0200 |
repaired copy_nam
|
file | diff | annotate |
Tue, 14 Sep 2010 12:12:42 +0200 |
adapted is_copy_named from v___ to v'''
|
file | diff | annotate |
Mon, 13 Sep 2010 18:37:16 +0200 |
tuned
|
file | diff | annotate |
Mon, 13 Sep 2010 18:12:15 +0200 |
ref --> Unsynchronized.ref tuned.
|
file | diff | annotate |
Mon, 13 Sep 2010 17:21:22 +0200 |
ref --> Unsynchronized.ref done
|
file | diff | annotate |
Mon, 13 Sep 2010 16:36:14 +0200 |
tuned, before changing ref --> Unsynchronized.ref
|
file | diff | annotate |
Mon, 13 Sep 2010 15:42:03 +0200 |
added src/Tools/isac/ROOT.ML
|
file | diff | annotate |
Fri, 10 Sep 2010 10:36:41 +0200 |
updated Knowledge/Test.thy
|
file | diff | annotate |
Thu, 09 Sep 2010 13:39:30 +0200 |
updated Knowledge/AlgEin.thy
|
file | diff | annotate |
Thu, 09 Sep 2010 09:58:28 +0200 |
updated Knowledge/EqSystem.thy
|
file | diff | annotate |
Thu, 09 Sep 2010 09:49:14 +0200 |
intermediate state in Knowledge/EqSystem.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 17:55:08 +0200 |
updated Knowledge/Integrate.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 17:49:36 +0200 |
updated Knowledge/DiffApp.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 17:17:29 +0200 |
updated Knowledge/Diff.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 16:54:15 +0200 |
updated Vect..LogExp.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 16:28:24 +0200 |
updated Knowledge/PolyEq.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 12:41:04 +0200 |
updated Knowledge/RatEq.thy
|
file | diff | annotate |
Wed, 08 Sep 2010 10:15:51 +0200 |
updated Knowledge/RootEq.thy
|
file | diff | annotate |