Wed, 11 May 2011 14:58:07 +0200 |
Walther Neuper |
intermed. ctxt ..: Add_Given doesnt work due to wrong ctxt in Subproblem
decompose-isar
|
changeset |
files
|
Wed, 11 May 2011 08:25:40 +0200 |
Walther Neuper |
intermed. ctxt ..: interrupted -- make x+1=2 go through first
decompose-isar
|
changeset |
files
|
Wed, 11 May 2011 07:28:13 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Mon, 09 May 2011 10:43:43 +0200 |
Walther Neuper |
added Rational_Test.thy
decompose-isar
|
changeset |
files
|
Sun, 08 May 2011 19:14:48 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Fri, 06 May 2011 11:18:07 +0200 |
Walther Neuper |
intermed. ctxt ..: cleanup before start with Add_Given
decompose-isar
|
changeset |
files
|
Thu, 05 May 2011 14:21:54 +0200 |
Walther Neuper |
intermed. ctxt over all minisubpbl x+1=2
decompose-isar
|
changeset |
files
|
Thu, 05 May 2011 09:23:32 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Wed, 04 May 2011 14:07:51 +0200 |
Walther Neuper |
move specific src/Tools/isac/jEdit parallel to src/Tools/jEdit
decompose-isar
|
changeset |
files
|
Wed, 04 May 2011 14:04:53 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Wed, 04 May 2011 09:01:10 +0200 |
Walther Neuper |
update all "Pair" to "Product_Type.Pair"
decompose-isar
|
changeset |
files
|
Tue, 03 May 2011 16:23:07 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Tue, 03 May 2011 16:20:55 +0200 |
Walther Neuper |
provided all "x+1=2" with typeconstraint real ("equality" is just bool)
decompose-isar
|
changeset |
files
|
Tue, 03 May 2011 15:58:04 +0200 |
Walther Neuper |
tuned, tests work
decompose-isar
|
changeset |
files
|
Tue, 03 May 2011 11:16:55 +0200 |
Walther Neuper |
updated all 'Const ("Let"..' to 'Const ("HOL.Let"..'
decompose-isar
|
changeset |
files
|
Sun, 01 May 2011 17:16:57 +0200 |
Marco Steger |
improved doku
decompose-isar
|
changeset |
files
|
Fri, 29 Apr 2011 13:00:34 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Fri, 29 Apr 2011 12:53:46 +0200 |
Walther Neuper |
added draft for presentation
decompose-isar
|
changeset |
files
|
Fri, 29 Apr 2011 11:11:07 +0200 |
Walther Neuper |
adapted file names of isabelle team
decompose-isar
|
changeset |
files
|
Fri, 29 Apr 2011 10:02:14 +0200 |
Walther Neuper |
new directory names for isac-team members
decompose-isar
|
changeset |
files
|
Mon, 18 Apr 2011 15:53:36 +0200 |
Mathias Lehnfeld |
copyright name added
decompose-isar
|
changeset |
files
|
Mon, 18 Apr 2011 15:48:46 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Mon, 18 Apr 2011 15:24:57 +0200 |
Mathias Lehnfeld |
ctxt intro finished (no environments)
decompose-isar
|
changeset |
files
|
Mon, 18 Apr 2011 14:43:26 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Sat, 16 Apr 2011 10:19:45 +0200 |
Walther Neuper |
Apply_Method transfers ctxt from specification to interpretation
decompose-isar
|
changeset |
files
|
Fri, 15 Apr 2011 17:07:34 +0200 |
Mathias Lehnfeld |
intermed. ctxt integration - assumptions now in context
decompose-isar
|
changeset |
files
|
Fri, 15 Apr 2011 15:58:52 +0200 |
Walther Neuper |
added ctxt-test, updated get_assumptions_
decompose-isar
|
changeset |
files
|
Thu, 14 Apr 2011 09:36:00 +0200 |
Walther Neuper |
merged
decompose-isar
|
changeset |
files
|
Thu, 14 Apr 2011 09:35:50 +0200 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Mon, 11 Apr 2011 12:56:57 +0200 |
Mathias Lehnfeld |
intermed. ctxt introduction
decompose-isar
|
changeset |
files
|
Fri, 08 Apr 2011 15:16:08 +0200 |
Mathias Lehnfeld |
intermed. context integration: parse replaced in some cases
decompose-isar
|
changeset |
files
|
Thu, 07 Apr 2011 16:31:05 +0200 |
Mathias Lehnfeld |
intermed. context integration
decompose-isar
|
changeset |
files
|
Wed, 06 Apr 2011 18:01:02 +0200 |
Mathias Lehnfeld |
intermed. context introduction to specification phase
decompose-isar
|
changeset |
files
|
Mon, 04 Apr 2011 11:05:07 +0200 |
Mathias Lehnfeld |
intermed. context integration appl_add does not work
decompose-isar
|
changeset |
files
|
Mon, 21 Mar 2011 00:32:53 +0100 |
Mathias Lehnfeld |
intermed. context integration: Isac compiles.
decompose-isar
|
changeset |
files
|
Wed, 23 Mar 2011 19:01:01 +0100 |
Walther Neuper |
make Test_Isac.thy run in jEdit finished
decompose-isar
|
changeset |
files
|
Wed, 23 Mar 2011 17:56:19 +0100 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Wed, 23 Mar 2011 17:54:38 +0100 |
Walther Neuper |
make Test_Isac.thy run in jEdit; intermed.: emacs runs
decompose-isar
|
changeset |
files
|
Wed, 23 Mar 2011 17:23:06 +0100 |
Walther Neuper |
added test for file dependencies in jEdit
decompose-isar
|
changeset |
files
|
Wed, 23 Mar 2011 17:20:39 +0100 |
Walther Neuper |
make Test_Isac.thy run in jEdit; intermed.
decompose-isar
|
changeset |
files
|
Sat, 19 Mar 2011 15:18:10 +0100 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Sat, 19 Mar 2011 15:09:19 +0100 |
Mathias Lehnfeld |
changes only for testing
decompose-isar
|
changeset |
files
|
Sat, 19 Mar 2011 15:03:36 +0100 |
Walther Neuper |
intermed. usecase Diophant: usecase1 shifted into test/../mathengine.sml
decompose-isar
|
changeset |
files
|
Sat, 19 Mar 2011 14:27:29 +0100 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|
Sat, 19 Mar 2011 13:06:19 +0100 |
Walther Neuper |
intermed. usecase Diophant: usecase1 finished in Test_Isac.thy
decompose-isar
|
changeset |
files
|
Fri, 18 Mar 2011 18:27:10 +0100 |
Walther Neuper |
intermed. usecase Diophant: 2 steps decomposed
decompose-isar
|
changeset |
files
|
Fri, 18 Mar 2011 17:24:56 +0100 |
Walther Neuper |
intermed. usecase Diophant
decompose-isar
|
changeset |
files
|
Fri, 18 Mar 2011 12:42:28 +0100 |
Walther Neuper |
intermed. usecase Diophant: build, tests OK
decompose-isar
|
changeset |
files
|
Fri, 18 Mar 2011 12:33:12 +0100 |
Walther Neuper |
intermed. usecase Diophant: change usecase inttype
decompose-isar
|
changeset |
files
|
Fri, 18 Mar 2011 09:26:03 +0100 |
Walther Neuper |
intermed. usecase Diophant
decompose-isar
|
changeset |
files
|
Thu, 17 Mar 2011 10:46:02 +0100 |
Walther Neuper |
intermed usecase Diophant
decompose-isar
|
changeset |
files
|
Thu, 17 Mar 2011 10:11:18 +0100 |
Walther Neuper |
intermed. usecase Diophant
decompose-isar
|
changeset |
files
|
Mon, 14 Mar 2011 16:50:44 +0100 |
Walther Neuper |
intermed.update Isabelle2011: tests finished...
decompose-isar
|
changeset |
files
|
Thu, 10 Mar 2011 17:05:09 +0100 |
Walther Neuper |
intermed.update Isabelle2011: Not --> HOL.Not
decompose-isar
|
changeset |
files
|
Thu, 10 Mar 2011 16:04:00 +0100 |
Walther Neuper |
intermed.update Isabelle2011: HOL.True
decompose-isar
|
changeset |
files
|
Thu, 10 Mar 2011 15:19:26 +0100 |
Walther Neuper |
merged
decompose-isar
|
changeset |
files
|
Thu, 10 Mar 2011 15:16:13 +0100 |
Walther Neuper |
intermed.update Isabelle2011:
decompose-isar
|
changeset |
files
|
Thu, 10 Mar 2011 15:12:55 +0100 |
Walther Neuper |
intermed.update Isabelle2011: after fetch ?!?
decompose-isar
|
changeset |
files
|
Thu, 10 Mar 2011 12:45:58 +0100 |
Walther Neuper |
intermed.update Isabelle2011: HOL.Trueprop
decompose-isar
|
changeset |
files
|
Fri, 04 Mar 2011 11:45:02 +0100 |
Walther Neuper |
tuned
decompose-isar
|
changeset |
files
|