| 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:17:46 +0200 |
tuned
|
file | diff | annotate |
| Fri, 20 May 2011 08:12:51 +0200 |
tuned
|
file | diff | annotate |
| Fri, 20 May 2011 07:24:18 +0200 |
tuned
|
file | diff | annotate |
| Thu, 19 May 2011 19:28:22 +0200 |
intermed. ctxt ..: add preconds in solve..Apply_Method
|
file | diff | annotate |
| Wed, 18 May 2011 16:06:00 +0200 |
tuned
|
file | diff | annotate |
| Wed, 18 May 2011 11:58:48 +0200 |
intermed. ctxt ..: calculation x+1=2 goes through
|
file | diff | annotate |
| Tue, 17 May 2011 17:54:58 +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 15:02:43 +0200 |
tuned
|
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 13:59:05 +0200 |
tuned
|
file | diff | annotate |
| Sun, 15 May 2011 12:36:29 +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 |
| Sun, 15 May 2011 10:25:42 +0200 |
tuned
|
file | diff | annotate |
| Fri, 13 May 2011 17:19:38 +0200 |
intermed. ctxt ..: x+1=2 now goes until Check_elementwise
|
file | diff | annotate |
| Fri, 13 May 2011 14:15:59 +0200 |
tuned
|
file | diff | annotate |
| Fri, 13 May 2011 10:26:44 +0200 |
tuned
|
file | diff | annotate |
| Fri, 13 May 2011 09:28:38 +0200 |
tuned
|
file | diff | annotate |
| Thu, 12 May 2011 10:00:06 +0200 |
added test-sequence with mini_subpbl x+1=2
|
file | diff | annotate |
| Wed, 11 May 2011 16:51:30 +0200 |
intermed. ctxt ..: added ctxt to Subproblem'
|
file | diff | annotate |
| Wed, 11 May 2011 14:58:07 +0200 |
intermed. ctxt ..: Add_Given doesnt work due to wrong ctxt in Subproblem
|
file | diff | annotate |
| Wed, 11 May 2011 08:25:40 +0200 |
intermed. ctxt ..: interrupted -- make x+1=2 go through first
|
file | diff | annotate |
| Wed, 11 May 2011 07:28:13 +0200 |
tuned
|
file | diff | annotate |
| Mon, 09 May 2011 10:43:43 +0200 |
added Rational_Test.thy
|
file | diff | annotate |
| Sun, 08 May 2011 19:14:48 +0200 |
tuned
|
file | diff | annotate |
| Fri, 06 May 2011 11:18:07 +0200 |
intermed. ctxt ..: cleanup before start with Add_Given
|
file | diff | annotate |
| Thu, 05 May 2011 14:21:54 +0200 |
intermed. ctxt over all minisubpbl x+1=2
|
file | diff | annotate |
| Thu, 05 May 2011 09:23:32 +0200 |
tuned
|
file | diff | annotate |
| Wed, 04 May 2011 14:04:53 +0200 |
tuned
|
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 15:58:04 +0200 |
tuned, tests work
|
file | diff | annotate |
| Tue, 03 May 2011 11:16:55 +0200 |
updated all 'Const ("Let"..' to 'Const ("HOL.Let"..'
|
file | diff | annotate |
| Mon, 18 Apr 2011 15:24:57 +0200 |
ctxt intro finished (no environments)
|
file | diff | annotate |
| Fri, 15 Apr 2011 15:58:52 +0200 |
added ctxt-test, updated get_assumptions_
|
file | diff | annotate |
| Thu, 14 Apr 2011 09:36:00 +0200 |
merged
|
file | diff | annotate |
| Thu, 14 Apr 2011 09:35:50 +0200 |
tuned
|
file | diff | annotate |
| Thu, 07 Apr 2011 16:31:05 +0200 |
intermed. context integration
|
file | diff | annotate |
| Wed, 06 Apr 2011 18:01:02 +0200 |
intermed. context introduction to specification phase
|
file | diff | annotate |
| Wed, 23 Mar 2011 19:01:01 +0100 |
make Test_Isac.thy run in jEdit finished
|
file | diff | annotate |
| Wed, 23 Mar 2011 17:54:38 +0100 |
make Test_Isac.thy run in jEdit; intermed.: emacs runs
|
file | diff | annotate |
| Wed, 23 Mar 2011 17:20:39 +0100 |
make Test_Isac.thy run in jEdit; intermed.
|
file | diff | annotate |
| Mon, 11 Oct 2010 13:31:22 +0200 |
removed all ".thy" in src/ and test/
|
file | diff | annotate |
| Tue, 28 Sep 2010 07:28:10 +0200 |
repaired fun uminus_to_string, fun rewrite_terms_
|
file | diff | annotate |
| Mon, 27 Sep 2010 13:35:06 +0200 |
simplified testing by src/Tools/isac/Build_Test_Isac.thy
|
file | diff | annotate |
| Sat, 25 Sep 2010 16:49:33 +0200 |
rewrite_ returns assumptions without Trueprop (as was in Isabelle2002)
|
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 14:49:23 +0200 |
updated "op +", "op -", "op *". "HOL.divide" in src & test
|
file | diff | annotate |
| Thu, 23 Sep 2010 12:56:51 +0200 |
interrupted update test/../Knowledge/integrate.sml, repaired term2str
|
file | diff | annotate |
| Thu, 23 Sep 2010 08:54:26 +0200 |
tuned pbt's due to copy_named
|
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 | base |