Tue, 29 Sep 2009 14:26:33 +1000 Merge with isabelle dev changes.
Thomas Sewell <tsewell@nicta.com.au> [Tue, 29 Sep 2009 14:26:33 +1000] rev 32759
Merge with isabelle dev changes.
Tue, 29 Sep 2009 14:25:42 +1000 Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
Thomas Sewell <tsewell@nicta.com.au> [Tue, 29 Sep 2009 14:25:42 +1000] rev 32758
Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
Mon, 28 Sep 2009 15:37:19 +1000 Avoid a possible variable name conflict in instantiating a theorem.
Thomas Sewell <tsewell@nicta.com.au> [Mon, 28 Sep 2009 15:37:19 +1000] rev 32757
Avoid a possible variable name conflict in instantiating a theorem. Instantiating a theorem variable with new variables created a possible variable name conflict if a record was defined with a field named 'f', 'x' etc. Using variable indices of 1 avoids the problem.
Mon, 28 Sep 2009 14:16:01 +1000 Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au> [Mon, 28 Sep 2009 14:16:01 +1000] rev 32756
Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.
Mon, 28 Sep 2009 11:13:11 +1000 Merge record patch with updates from isabelle mainline.
Thomas Sewell <tsewell@nicta.com.au> [Mon, 28 Sep 2009 11:13:11 +1000] rev 32755
Merge record patch with updates from isabelle mainline.
Fri, 25 Sep 2009 19:04:18 +1000 Avoid record-inner constants in polymorphic definitions in Bali
Thomas Sewell <tsewell@nicta.com.au> [Fri, 25 Sep 2009 19:04:18 +1000] rev 32754
Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.
Thu, 24 Sep 2009 11:33:05 +1000 Merge with changes from isabelle dev repository.
Thomas Sewell <tsewell@nicta.com.au> [Thu, 24 Sep 2009 11:33:05 +1000] rev 32753
Merge with changes from isabelle dev repository.
Wed, 23 Sep 2009 19:17:48 +1000 Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au [Wed, 23 Sep 2009 19:17:48 +1000] rev 32752
Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.
Tue, 22 Sep 2009 13:52:19 +1000 Branch merge for isabelle mainline updates.
Thomas Sewell <tsewell@nicta.com.au> [Tue, 22 Sep 2009 13:52:19 +1000] rev 32751
Branch merge for isabelle mainline updates.
Thu, 17 Sep 2009 14:17:37 +1000 Branch merge with updates from mainline isabelle.
Thomas Sewell <tsewell@nicta.com.au> [Thu, 17 Sep 2009 14:17:37 +1000] rev 32750
Branch merge with updates from mainline isabelle.
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip