| Thu, 22 Dec 2016 11:36:20 +0100 |
renamed Ctree.ptree --> Ctree.ctree
|
file | diff | annotate |
| Thu, 22 Dec 2016 10:25:49 +0100 |
--- closed structure Ctree
|
file | diff | annotate |
| Wed, 21 Dec 2016 08:57:47 +0100 |
added structure Applicable INTERMEDIATELY
|
file | diff | annotate |
| Mon, 19 Dec 2016 10:37:44 +0100 |
renamed structure to Generate : GENERATE_CALC_TREE
|
file | diff | annotate |
| Sun, 18 Dec 2016 16:27:41 +0100 |
added structure Specify : MODEL_SPECIFY
|
file | diff | annotate |
| Wed, 14 Dec 2016 09:37:01 +0100 |
added structure Ctree : CALC_TREE
|
file | diff | annotate |
| Mon, 12 Dec 2016 18:08:13 +0100 |
added structure Chead : CALC_HEAD
|
file | diff | annotate |
| Wed, 30 Nov 2016 12:09:24 +0100 |
added structure Rtools : REWRITE_TOOLS
|
file | diff | annotate |
| Tue, 22 Nov 2016 10:42:21 +0100 |
added structure Math_Engine : MATH_ENGINE
|
file | diff | annotate |
| Mon, 21 Nov 2016 12:47:02 +0100 |
added structure Kernel: KERNEL
|
file | diff | annotate |
| Thu, 17 Nov 2016 16:40:27 +0100 |
close structures again after Test_Isac
|
file | diff | annotate |
| Mon, 14 Nov 2016 15:51:10 +0100 |
LUCAS_INTERPRETER works in tests
|
file | diff | annotate |
| Sat, 12 Nov 2016 17:21:43 +0100 |
--- polished LUCAS_INTERPRETER
|
file | diff | annotate |
| Thu, 20 Oct 2016 10:26:29 +0200 |
simplify handling of theorems
|
file | diff | annotate |
| Tue, 18 Oct 2016 12:05:03 +0200 |
back-track after desing error in previous changeset
|
file | diff | annotate |
| Mon, 10 Oct 2016 18:24:14 +0200 |
transport terms in theorems to frontend
|
file | diff | annotate |
| Sat, 27 Aug 2016 16:57:18 +0200 |
improve error messages for writing Isac programs
|
file | diff | annotate |
| Mon, 07 Dec 2015 11:25:02 +0100 |
Isabelle2014-->15: term_of-->Thm.term_of
|
file | diff | annotate |
| Mon, 07 Dec 2015 10:52:07 +0100 |
Isabelle2014-->15: Thm.thy is not open anymore, further funs qualified
|
file | diff | annotate |
| Mon, 07 Dec 2015 10:17:08 +0100 |
sabelle2014-->15: cterm_of-->Thm.global_cterm_of
|
file | diff | annotate |
| Fri, 13 Jun 2014 09:55:49 +0200 |
trivial removals of the_generic_context done.
|
file | diff | annotate |
| Fri, 06 Jun 2014 06:50:02 +0200 |
removed further Unsynchronized.ref
|
file | diff | annotate |
| Thu, 24 Oct 2013 00:02:29 +0100 |
switched from "calclist' = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Thu, 10 Oct 2013 19:16:16 +0100 |
restrict access to "calclist' = Unsynchronized.ref"
|
file | diff | annotate |
| Mon, 22 Jul 2013 13:52:18 +0200 |
--- Test_Isac.thy runs all tests
|
file | diff | annotate |
| Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
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 |
| Wed, 13 Jun 2012 07:28:39 +0200 |
first dialog sequence for error patterns
|
file | diff | annotate |
| Sat, 17 Mar 2012 11:06:46 +0100 |
uncomment test/../rateq.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Sat, 10 Mar 2012 09:41:09 +0100 |
uncomment test/../biegelinie (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Sun, 08 Jan 2012 08:41:35 +0100 |
Build_Inverse_Z_Transform ready for continuation
|
file | diff | annotate |
| Sat, 07 Jan 2012 10:06:06 +0100 |
invisible changes in calculations are possible now.
|
file | diff | annotate |
| Fri, 23 Sep 2011 13:58:27 +0200 |
tuned
|
file | diff | annotate |
| Fri, 23 Sep 2011 09:41:11 +0200 |
repair ctxt in assy, ass_up, astep_up done.
|
file | diff | annotate |
| Fri, 23 Sep 2011 08:30:35 +0200 |
repair ctxt in locate_gen
|
file | diff | annotate |
| Sat, 10 Sep 2011 10:37:24 +0200 |
method ["PolyEq", "solve_d2_polyeq_pq_equation"] works for jrocnik
|
file | diff | annotate |
| Wed, 07 Sep 2011 10:07:13 +0200 |
intermed. pqformula for Z-transform
|
file | diff | annotate |
| Wed, 20 Jul 2011 14:55:29 +0200 |
removed error in some PolyEq.program
|
file | diff | annotate |
| Mon, 18 Jul 2011 09:29:17 +0200 |
intermed: make autocalc..CompleteCalc run with x+1=2
|
file | diff | annotate |
| Thu, 14 Jul 2011 09:33:57 +0200 |
added ADDTESTS/course/ml_quickstart/ML2_Functions.thy
|
file | diff | annotate |
| Sat, 21 May 2011 12:52:59 +0200 |
intermed. ctxt .. FINISHED
|
file | diff | annotate |
| Fri, 20 May 2011 14:49:07 +0200 |
tuned
|
file | diff | annotate |
| Fri, 20 May 2011 13:43:25 +0200 |
intermed. ctxt ..: generate1..Check_Postcond..(*map str2term asm*)
|
file | diff | annotate |
| Fri, 20 May 2011 09:12:40 +0200 |
intermed. ctxt ..: init_scrstate without precond work
|
file | diff | annotate |
| Fri, 20 May 2011 08:32:57 +0200 |
intermed. ctxt ..: taken from fun init_scrstate
|
file | diff | annotate |
| Fri, 20 May 2011 08:12:51 +0200 |
tuned
|
file | diff | annotate |
| Wed, 18 May 2011 11:58:48 +0200 |
intermed. ctxt ..: calculation x+1=2 goes through
|
file | diff | annotate |
| Wed, 18 May 2011 10:20:11 +0200 |
intermed. ctxt ..: checked all generate1
|
file | diff | annotate |
| Wed, 18 May 2011 09:32:26 +0200 |
tuned
|
file | diff | annotate |
| Wed, 18 May 2011 08:47:10 +0200 |
tuned
|
file | diff | annotate |
| Tue, 17 May 2011 17:38:35 +0200 |
intermed. ctxt ..: ctxt correct after Apply_Method in sub-method
|
file | diff | annotate |
| Tue, 17 May 2011 14:56:54 +0200 |
intermed. ctxt ..: finished check e_ctxt
|
file | diff | annotate |
| Tue, 17 May 2011 09:55:30 +0200 |
tuned
|
file | diff | annotate |
| Sun, 15 May 2011 11:32:41 +0200 |
intermed. ctxt ..: checked all occurrences of ProofContext.init_global
|
file | diff | annotate |
| Fri, 13 May 2011 17:19:38 +0200 |
intermed. ctxt ..: x+1=2 now goes until Check_elementwise
|
file | diff | annotate |
| Thu, 12 May 2011 08:26:02 +0200 |
tuned
|
file | diff | annotate |
| Wed, 11 May 2011 16:51:30 +0200 |
intermed. ctxt ..: added ctxt to Subproblem'
|
file | diff | annotate |
| Wed, 04 May 2011 09:01:10 +0200 |
update all "Pair" to "Product_Type.Pair"
|
file | diff | annotate |
| Tue, 03 May 2011 11:16:55 +0200 |
updated all 'Const ("Let"..' to 'Const ("HOL.Let"..'
|
file | diff | annotate |