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 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip