# HG changeset patch
# User wenzelm
# Date 1323874215 -3600
# Node ID 7887eabb1997e3459e4a4a284f3e9784cf43a870
# Parent  a8b9191609a8717f30335ae9ea004db4ba75f2e6# Parent  afdb92130f5a4131dd0305a33583397dd00bb8e5
merged

diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/Brackin.thy
--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
-
-A couple from Steve Brackin's work.
-*)
-
-theory Brackin imports Main begin
-
-datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
-                X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
-                X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
-                X32 | X33 | X34
-
-datatype  
-  ('a, 'b, 'c) TY1 =
-      NoF__
-    | Fk__ 'a "('a, 'b, 'c) TY2"
-and
-  ('a, 'b, 'c) TY2 =
-      Ta__ bool
-    | Td__ bool
-    | Tf__ "('a, 'b, 'c) TY1"
-    | Tk__ bool
-    | Tp__ bool
-    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
-    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
-and
-  ('a, 'b, 'c) TY3 =
-      NoS__
-    | Fresh__ "('a, 'b, 'c) TY2"
-    | Trustworthy__ 'a
-    | PrivateKey__ 'a 'b 'c
-    | PublicKey__ 'a 'b 'c
-    | Conveyed__ 'a "('a, 'b, 'c) TY2"
-    | Possesses__ 'a "('a, 'b, 'c) TY2"
-    | Received__ 'a "('a, 'b, 'c) TY2"
-    | Recognizes__ 'a "('a, 'b, 'c) TY2"
-    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
-    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
-    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
-    | Believes__ 'a "('a, 'b, 'c) TY3"
-    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
-
-end
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/Instructions.thy
--- a/Admin/Benchmarks/HOL-datatype/Instructions.thy	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/Instructions.thy
-
-Example from Konrad: 68000 instruction set.
-*)
-
-theory Instructions imports Main begin
-
-datatype Size = Byte | Word | Long
-
-datatype DataRegister
-              = RegD0
-              | RegD1
-              | RegD2
-              | RegD3
-              | RegD4
-              | RegD5
-              | RegD6
-              | RegD7
-
-datatype AddressRegister
-              = RegA0
-              | RegA1
-              | RegA2
-              | RegA3
-              | RegA4
-              | RegA5
-              | RegA6
-              | RegA7
-
-datatype DataOrAddressRegister
-              = data DataRegister
-              | address AddressRegister
-
-datatype Condition
-              = Hi
-              | Ls
-              | Cc
-              | Cs
-              | Ne
-              | Eq
-              | Vc
-              | Vs
-              | Pl
-              | Mi
-              | Ge
-              | Lt
-              | Gt
-              | Le
-
-datatype AddressingMode
-        = immediate nat
-        | direct DataOrAddressRegister
-        | indirect AddressRegister
-        | postinc AddressRegister
-        | predec AddressRegister
-        | indirectdisp nat AddressRegister
-        | indirectindex nat AddressRegister DataOrAddressRegister Size
-        | absolute nat
-        | pcdisp nat
-        | pcindex nat DataOrAddressRegister Size
-
-datatype M68kInstruction
-    = ABCD AddressingMode AddressingMode
-    | ADD Size AddressingMode AddressingMode
-    | ADDA Size AddressingMode AddressRegister
-    | ADDI Size nat AddressingMode
-    | ADDQ Size nat AddressingMode
-    | ADDX Size AddressingMode AddressingMode
-    | AND Size AddressingMode AddressingMode
-    | ANDI Size nat AddressingMode
-    | ANDItoCCR nat
-    | ANDItoSR nat
-    | ASL Size AddressingMode DataRegister
-    | ASLW AddressingMode
-    | ASR Size AddressingMode DataRegister
-    | ASRW AddressingMode
-    | Bcc Condition Size nat
-    | BTST Size AddressingMode AddressingMode
-    | BCHG Size AddressingMode AddressingMode
-    | BCLR Size AddressingMode AddressingMode
-    | BSET Size AddressingMode AddressingMode
-    | BRA Size nat
-    | BSR Size nat
-    | CHK AddressingMode DataRegister
-    | CLR Size AddressingMode
-    | CMP Size AddressingMode DataRegister
-    | CMPA Size AddressingMode AddressRegister
-    | CMPI Size nat AddressingMode
-    | CMPM Size AddressRegister AddressRegister
-    | DBT DataRegister nat
-    | DBF DataRegister nat
-    | DBcc Condition DataRegister nat
-    | DIVS AddressingMode DataRegister
-    | DIVU AddressingMode DataRegister
-    | EOR Size DataRegister AddressingMode
-    | EORI Size nat AddressingMode
-    | EORItoCCR nat
-    | EORItoSR nat
-    | EXG DataOrAddressRegister DataOrAddressRegister
-    | EXT Size DataRegister
-    | ILLEGAL
-    | JMP AddressingMode
-    | JSR AddressingMode
-    | LEA AddressingMode AddressRegister
-    | LINK AddressRegister nat
-    | LSL Size AddressingMode DataRegister
-    | LSLW AddressingMode
-    | LSR Size AddressingMode DataRegister
-    | LSRW AddressingMode
-    | MOVE Size AddressingMode AddressingMode
-    | MOVEtoCCR AddressingMode
-    | MOVEtoSR AddressingMode
-    | MOVEfromSR AddressingMode
-    | MOVEtoUSP AddressingMode
-    | MOVEfromUSP AddressingMode
-    | MOVEA Size AddressingMode AddressRegister
-    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
-    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
-    | MOVEP Size AddressingMode AddressingMode
-    | MOVEQ nat DataRegister
-    | MULS AddressingMode DataRegister
-    | MULU AddressingMode DataRegister
-    | NBCD AddressingMode
-    | NEG Size AddressingMode
-    | NEGX Size AddressingMode
-    | NOP
-    | NOT Size AddressingMode
-    | OR Size AddressingMode AddressingMode
-    | ORI Size nat AddressingMode
-    | ORItoCCR nat
-    | ORItoSR nat
-    | PEA AddressingMode
-    | RESET
-    | ROL Size AddressingMode DataRegister
-    | ROLW AddressingMode
-    | ROR Size AddressingMode DataRegister
-    | RORW AddressingMode
-    | ROXL Size AddressingMode DataRegister
-    | ROXLW AddressingMode
-    | ROXR Size AddressingMode DataRegister
-    | ROXRW AddressingMode
-    | RTE
-    | RTR
-    | RTS
-    | SBCD AddressingMode AddressingMode
-    | ST AddressingMode
-    | SF AddressingMode
-    | Scc Condition AddressingMode
-    | STOP nat
-    | SUB Size AddressingMode AddressingMode
-    | SUBA Size AddressingMode AddressingMode
-    | SUBI Size nat AddressingMode
-    | SUBQ Size nat AddressingMode
-    | SUBX Size AddressingMode AddressingMode
-    | SWAP DataRegister
-    | TAS AddressingMode
-    | TRAP nat
-    | TRAPV
-    | TST Size AddressingMode
-    | UNLK AddressRegister
-
-end
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
-
-Some rather large datatype examples (from John Harrison).
-*)
-
-val tests = ["Brackin", "Instructions", "SML", "Verilog"];
-
-Toplevel.timing := true;
-
-warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
-use_thys tests;
-
-warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
-List.app Thy_Info.remove_thy tests;
-use_thys tests;
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/SML.thy
--- a/Admin/Benchmarks/HOL-datatype/SML.thy	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/SML.thy
-
-Example from Myra: part of the syntax of SML.
-*)
-
-theory SML imports Main begin
-
-datatype
-  string = EMPTY_STRING | CONS_STRING nat string
-
-datatype
-   strid = STRID string
-
-datatype
-   var = VAR string
-
-datatype
-   con = CON string
-
-datatype
-   scon = SCINT nat | SCSTR string
-
-datatype
-   excon = EXCON string
-
-datatype
-   label = LABEL string
-
-datatype
-  'a nonemptylist = Head_and_tail 'a "'a list"
-
-datatype
-  'a long = BASE 'a | QUALIFIED strid "'a long"
-
-datatype
-   atpat_e = WILDCARDatpat_e
-           | SCONatpat_e scon
-           | VARatpat_e var
-           | CONatpat_e "con long"
-           | EXCONatpat_e "excon long"
-           | RECORDatpat_e "patrow_e option"
-           | PARatpat_e pat_e
-and
-   patrow_e = DOTDOTDOT_e
-            | PATROW_e label pat_e "patrow_e option"
-and
-   pat_e = ATPATpat_e atpat_e
-         | CONpat_e "con long" atpat_e
-         | EXCONpat_e "excon long" atpat_e
-         | LAYEREDpat_e var pat_e
-and
-   conbind_e = CONBIND_e con "conbind_e option"
-and
-   datbind_e = DATBIND_e conbind_e "datbind_e option"
-and
-   exbind_e = EXBIND1_e excon "exbind_e option"
-            | EXBIND2_e excon "excon long" "exbind_e option"
-and
-   atexp_e = SCONatexp_e scon
-           | VARatexp_e "var long"
-           | CONatexp_e "con long"
-           | EXCONatexp_e "excon long"
-           | RECORDatexp_e "exprow_e option"
-           | LETatexp_e dec_e exp_e
-           | PARatexp_e exp_e
-and
-   exprow_e = EXPROW_e label exp_e "exprow_e option"
-and
-   exp_e = ATEXPexp_e atexp_e
-         | APPexp_e exp_e atexp_e
-         | HANDLEexp_e exp_e match_e
-         | RAISEexp_e exp_e
-         | FNexp_e match_e
-and
-   match_e = MATCH_e mrule_e "match_e option"
-and
-   mrule_e = MRULE_e pat_e exp_e
-and
-   dec_e = VALdec_e valbind_e
-         | DATATYPEdec_e datbind_e
-         | ABSTYPEdec_e datbind_e dec_e
-         | EXCEPTdec_e exbind_e
-         | LOCALdec_e dec_e dec_e
-         | OPENdec_e "strid long nonemptylist"
-         | EMPTYdec_e
-         | SEQdec_e dec_e dec_e
-and
-   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
-             | RECvalbind_e valbind_e
-
-end
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/Verilog.thy
--- a/Admin/Benchmarks/HOL-datatype/Verilog.thy	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
-
-Example from Daryl: a Verilog grammar.
-*)
-
-theory Verilog imports Main begin
-
-datatype
-  Source_text
-     = module string "string list" "Module_item list"
-     | Source_textMeta string
-and
-  Module_item
-     = "declaration" Declaration
-     | initial Statement
-     | always Statement
-     | assign Lvalue Expression
-     | Module_itemMeta string
-and
-  Declaration
-     = reg_declaration "Range option" "string list"
-     | net_declaration "Range option" "string list"
-     | input_declaration "Range option" "string list"
-     | output_declaration "Range option" "string list"
-     | DeclarationMeta string
-and
-  Range = range Expression Expression | RangeMeta string
-and
-  Statement
-     = clock_statement Clock Statement_or_null
-     | blocking_assignment Lvalue Expression
-     | non_blocking_assignment Lvalue Expression
-     | conditional_statement
-          Expression Statement_or_null "Statement_or_null option"
-     | case_statement Expression "Case_item list"
-     | while_loop Expression Statement
-     | repeat_loop Expression Statement
-     | for_loop
-          Lvalue Expression Expression Lvalue Expression Statement
-     | forever_loop Statement
-     | disable string
-     | seq_block "string option" "Statement list"
-     | StatementMeta string
-and
-  Statement_or_null
-     = statement Statement | null_statement | Statement_or_nullMeta string
-and
-  Clock
-     = posedge string
-     | negedge string
-     | clock string
-     | ClockMeta string
-and
-  Case_item
-     = case_item "Expression list" Statement_or_null
-     | default_case_item Statement_or_null
-     | Case_itemMeta string
-and
-  Expression
-     = plus Expression Expression
-     | minus Expression Expression
-     | lshift Expression Expression
-     | rshift Expression Expression
-     | lt Expression Expression
-     | leq Expression Expression
-     | gt Expression Expression
-     | geq Expression Expression
-     | logeq Expression Expression
-     | logneq Expression Expression
-     | caseeq Expression Expression
-     | caseneq Expression Expression
-     | bitand Expression Expression
-     | bitxor Expression Expression
-     | bitor Expression Expression
-     | logand Expression Expression
-     | logor Expression Expression
-     | conditional Expression Expression Expression
-     | positive Primary
-     | negative Primary
-     | lognot Primary
-     | bitnot Primary
-     | reducand Primary
-     | reducxor Primary
-     | reducor Primary
-     | reducnand Primary
-     | reducxnor Primary
-     | reducnor Primary
-     | primary Primary
-     | ExpressionMeta string
-and
-  Primary
-     = primary_number Number
-     | primary_IDENTIFIER string
-     | primary_bit_select string Expression
-     | primary_part_select string Expression Expression
-     | primary_gen_bit_select Expression Expression
-     | primary_gen_part_select Expression Expression Expression
-     | primary_concatenation Concatenation
-     | primary_multiple_concatenation Multiple_concatenation
-     | brackets Expression
-     | PrimaryMeta string
-and
-  Lvalue
-     = lvalue string
-     | lvalue_bit_select string Expression
-     | lvalue_part_select string Expression Expression
-     | lvalue_concatenation Concatenation
-     | LvalueMeta string
-and
-  Number
-     = decimal string
-     | based "string option" string
-     | NumberMeta string
-and
-  Concatenation
-     = concatenation "Expression list" | ConcatenationMeta string
-and
-  Multiple_concatenation
-     = multiple_concatenation Expression "Expression list"
-     | Multiple_concatenationMeta string
-and
-  meta
-     = Meta_Source_text Source_text
-     | Meta_Module_item Module_item
-     | Meta_Declaration Declaration
-     | Meta_Range Range
-     | Meta_Statement Statement
-     | Meta_Statement_or_null Statement_or_null
-     | Meta_Clock Clock
-     | Meta_Case_item Case_item
-     | Meta_Expression Expression
-     | Meta_Primary Primary
-     | Meta_Lvalue Lvalue
-     | Meta_Number Number
-     | Meta_Concatenation Concatenation
-     | Meta_Multiple_concatenation Multiple_concatenation
-
-end
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-record/ROOT.ML
--- a/Admin/Benchmarks/HOL-record/ROOT.ML	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-record/ROOT.ML
-
-Some benchmark on large record.
-*)
-
-val tests = ["Record_Benchmark"];
-
-Toplevel.timing := true;
-
-warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
-use_thys tests;
-
-warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
-use_thys tests;
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-record/Record_Benchmark.thy
--- a/Admin/Benchmarks/HOL-record/Record_Benchmark.thy	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-record/Record_Benchmark.thy
-    Author:     Norbert Schirmer, DFKI
-*)
-
-header {* Benchmark for large record *}
-
-theory Record_Benchmark
-imports Main
-begin
-
-declare [[record_timing]]
-
-record many_A =
-A000::nat
-A001::nat
-A002::nat
-A003::nat
-A004::nat
-A005::nat
-A006::nat
-A007::nat
-A008::nat
-A009::nat
-A010::nat
-A011::nat
-A012::nat
-A013::nat
-A014::nat
-A015::nat
-A016::nat
-A017::nat
-A018::nat
-A019::nat
-A020::nat
-A021::nat
-A022::nat
-A023::nat
-A024::nat
-A025::nat
-A026::nat
-A027::nat
-A028::nat
-A029::nat
-A030::nat
-A031::nat
-A032::nat
-A033::nat
-A034::nat
-A035::nat
-A036::nat
-A037::nat
-A038::nat
-A039::nat
-A040::nat
-A041::nat
-A042::nat
-A043::nat
-A044::nat
-A045::nat
-A046::nat
-A047::nat
-A048::nat
-A049::nat
-A050::nat
-A051::nat
-A052::nat
-A053::nat
-A054::nat
-A055::nat
-A056::nat
-A057::nat
-A058::nat
-A059::nat
-A060::nat
-A061::nat
-A062::nat
-A063::nat
-A064::nat
-A065::nat
-A066::nat
-A067::nat
-A068::nat
-A069::nat
-A070::nat
-A071::nat
-A072::nat
-A073::nat
-A074::nat
-A075::nat
-A076::nat
-A077::nat
-A078::nat
-A079::nat
-A080::nat
-A081::nat
-A082::nat
-A083::nat
-A084::nat
-A085::nat
-A086::nat
-A087::nat
-A088::nat
-A089::nat
-A090::nat
-A091::nat
-A092::nat
-A093::nat
-A094::nat
-A095::nat
-A096::nat
-A097::nat
-A098::nat
-A099::nat
-A100::nat
-A101::nat
-A102::nat
-A103::nat
-A104::nat
-A105::nat
-A106::nat
-A107::nat
-A108::nat
-A109::nat
-A110::nat
-A111::nat
-A112::nat
-A113::nat
-A114::nat
-A115::nat
-A116::nat
-A117::nat
-A118::nat
-A119::nat
-A120::nat
-A121::nat
-A122::nat
-A123::nat
-A124::nat
-A125::nat
-A126::nat
-A127::nat
-A128::nat
-A129::nat
-A130::nat
-A131::nat
-A132::nat
-A133::nat
-A134::nat
-A135::nat
-A136::nat
-A137::nat
-A138::nat
-A139::nat
-A140::nat
-A141::nat
-A142::nat
-A143::nat
-A144::nat
-A145::nat
-A146::nat
-A147::nat
-A148::nat
-A149::nat
-A150::nat
-A151::nat
-A152::nat
-A153::nat
-A154::nat
-A155::nat
-A156::nat
-A157::nat
-A158::nat
-A159::nat
-A160::nat
-A161::nat
-A162::nat
-A163::nat
-A164::nat
-A165::nat
-A166::nat
-A167::nat
-A168::nat
-A169::nat
-A170::nat
-A171::nat
-A172::nat
-A173::nat
-A174::nat
-A175::nat
-A176::nat
-A177::nat
-A178::nat
-A179::nat
-A180::nat
-A181::nat
-A182::nat
-A183::nat
-A184::nat
-A185::nat
-A186::nat
-A187::nat
-A188::nat
-A189::nat
-A190::nat
-A191::nat
-A192::nat
-A193::nat
-A194::nat
-A195::nat
-A196::nat
-A197::nat
-A198::nat
-A199::nat
-A200::nat
-A201::nat
-A202::nat
-A203::nat
-A204::nat
-A205::nat
-A206::nat
-A207::nat
-A208::nat
-A209::nat
-A210::nat
-A211::nat
-A212::nat
-A213::nat
-A214::nat
-A215::nat
-A216::nat
-A217::nat
-A218::nat
-A219::nat
-A220::nat
-A221::nat
-A222::nat
-A223::nat
-A224::nat
-A225::nat
-A226::nat
-A227::nat
-A228::nat
-A229::nat
-A230::nat
-A231::nat
-A232::nat
-A233::nat
-A234::nat
-A235::nat
-A236::nat
-A237::nat
-A238::nat
-A239::nat
-A240::nat
-A241::nat
-A242::nat
-A243::nat
-A244::nat
-A245::nat
-A246::nat
-A247::nat
-A248::nat
-A249::nat
-A250::nat
-A251::nat
-A252::nat
-A253::nat
-A254::nat
-A255::nat
-A256::nat
-A257::nat
-A258::nat
-A259::nat
-A260::nat
-A261::nat
-A262::nat
-A263::nat
-A264::nat
-A265::nat
-A266::nat
-A267::nat
-A268::nat
-A269::nat
-A270::nat
-A271::nat
-A272::nat
-A273::nat
-A274::nat
-A275::nat
-A276::nat
-A277::nat
-A278::nat
-A279::nat
-A280::nat
-A281::nat
-A282::nat
-A283::nat
-A284::nat
-A285::nat
-A286::nat
-A287::nat
-A288::nat
-A289::nat
-A290::nat
-A291::nat
-A292::nat
-A293::nat
-A294::nat
-A295::nat
-A296::nat
-A297::nat
-A298::nat
-A299::nat
-
-lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
-  by simp
-
-lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
-  by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-  by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
-  done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
-  apply simp
-  done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-  apply simp
-  done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
-  apply simp
-  done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-  apply simp
-  done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
-  apply auto
-  done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-  apply auto
-  done
-
-lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-  apply auto
-  done
-
-lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-  apply auto
-  done
-
-
-lemma True
-proof -
-  {
-    fix P r
-    assume pre: "P (A155 r)"
-    have "\<exists>x. P x"
-      using pre
-      apply -
-      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-      apply auto 
-      done
-  }
-  show ?thesis ..
-qed
-
-
-lemma "\<exists>r. A155 r = x"
-  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
-  done
-
-
-end
\ No newline at end of file
diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/IsaMakefile
--- a/Admin/Benchmarks/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-
-## targets
-
-default: all
-images:
-test: HOL-datatype HOL-record
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-
-## HOL-datatype
-
-HOL:
-	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-
-
-HOL-datatype: HOL $(LOG)/HOL-datatype.gz
-
-$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/ROOT.ML		\
-  HOL-datatype/Brackin.thy HOL-datatype/Instructions.thy	\
-  HOL-datatype/SML.thy HOL-datatype/Verilog.thy
-	@$(ISABELLE_TOOL) usedir -s datatype $(OUT)/HOL HOL-datatype
-
-
-## HOL-record
-
-HOL-record: HOL $(LOG)/HOL-record.gz
-
-$(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML	\
-   HOL-record/Record_Benchmark.thy
-	@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz
diff -r a8b9191609a8 -r 7887eabb1997 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Wed Dec 14 15:05:22 2011 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Dec 14 15:50:15 2011 +0100
@@ -46,6 +46,8 @@
 
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
+TARGETS=all
+
 # make file flags and nice setup for different target platforms
 case $HOSTNAME in
     atbroy51)
@@ -69,6 +71,7 @@
   
     macbroy2)
         MFLAGS="-k"
+        TARGETS=full
         NICE=""
         ;;
 
@@ -97,6 +100,12 @@
         NICE=""
         ;;
 
+    macbroy30)
+        MFLAGS="-k"
+        TARGETS=full
+        NICE=""
+        ;;
+
     *)
         MFLAGS="-k"
         # be nice by default
@@ -119,7 +128,7 @@
   TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
 else
   DIR="."
-  TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
+  TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
 fi
 
 IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
diff -r a8b9191609a8 -r 7887eabb1997 src/CCL/IsaMakefile
--- a/src/CCL/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/CCL/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: CCL
 test: CCL-ex
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/CTT/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: CTT
 test: CTT-ex
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/Cube/IsaMakefile
--- a/src/Cube/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/Cube/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images:
 test: Pure-Cube
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/FOL/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: FOL
 test: FOL-ex
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/FOLP/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: FOLP
 test: FOLP-ex
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Datatype_Benchmark/Brackin.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/Brackin.thy	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Datatype_Benchmark/Brackin.thy
+
+A couple from Steve Brackin's work.
+*)
+
+theory Brackin imports Main begin
+
+datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
+                X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
+                X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
+                X32 | X33 | X34
+
+datatype  
+  ('a, 'b, 'c) TY1 =
+      NoF__
+    | Fk__ 'a "('a, 'b, 'c) TY2"
+and
+  ('a, 'b, 'c) TY2 =
+      Ta__ bool
+    | Td__ bool
+    | Tf__ "('a, 'b, 'c) TY1"
+    | Tk__ bool
+    | Tp__ bool
+    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
+and
+  ('a, 'b, 'c) TY3 =
+      NoS__
+    | Fresh__ "('a, 'b, 'c) TY2"
+    | Trustworthy__ 'a
+    | PrivateKey__ 'a 'b 'c
+    | PublicKey__ 'a 'b 'c
+    | Conveyed__ 'a "('a, 'b, 'c) TY2"
+    | Possesses__ 'a "('a, 'b, 'c) TY2"
+    | Received__ 'a "('a, 'b, 'c) TY2"
+    | Recognizes__ 'a "('a, 'b, 'c) TY2"
+    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
+    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
+    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
+    | Believes__ 'a "('a, 'b, 'c) TY3"
+    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
+
+end
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Datatype_Benchmark/Instructions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/Instructions.thy	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,162 @@
+(*  Title:      HOL/Datatype_Benchmark/Instructions.thy
+
+Example from Konrad: 68000 instruction set.
+*)
+
+theory Instructions imports Main begin
+
+datatype Size = Byte | Word | Long
+
+datatype DataRegister
+              = RegD0
+              | RegD1
+              | RegD2
+              | RegD3
+              | RegD4
+              | RegD5
+              | RegD6
+              | RegD7
+
+datatype AddressRegister
+              = RegA0
+              | RegA1
+              | RegA2
+              | RegA3
+              | RegA4
+              | RegA5
+              | RegA6
+              | RegA7
+
+datatype DataOrAddressRegister
+              = data DataRegister
+              | address AddressRegister
+
+datatype Condition
+              = Hi
+              | Ls
+              | Cc
+              | Cs
+              | Ne
+              | Eq
+              | Vc
+              | Vs
+              | Pl
+              | Mi
+              | Ge
+              | Lt
+              | Gt
+              | Le
+
+datatype AddressingMode
+        = immediate nat
+        | direct DataOrAddressRegister
+        | indirect AddressRegister
+        | postinc AddressRegister
+        | predec AddressRegister
+        | indirectdisp nat AddressRegister
+        | indirectindex nat AddressRegister DataOrAddressRegister Size
+        | absolute nat
+        | pcdisp nat
+        | pcindex nat DataOrAddressRegister Size
+
+datatype M68kInstruction
+    = ABCD AddressingMode AddressingMode
+    | ADD Size AddressingMode AddressingMode
+    | ADDA Size AddressingMode AddressRegister
+    | ADDI Size nat AddressingMode
+    | ADDQ Size nat AddressingMode
+    | ADDX Size AddressingMode AddressingMode
+    | AND Size AddressingMode AddressingMode
+    | ANDI Size nat AddressingMode
+    | ANDItoCCR nat
+    | ANDItoSR nat
+    | ASL Size AddressingMode DataRegister
+    | ASLW AddressingMode
+    | ASR Size AddressingMode DataRegister
+    | ASRW AddressingMode
+    | Bcc Condition Size nat
+    | BTST Size AddressingMode AddressingMode
+    | BCHG Size AddressingMode AddressingMode
+    | BCLR Size AddressingMode AddressingMode
+    | BSET Size AddressingMode AddressingMode
+    | BRA Size nat
+    | BSR Size nat
+    | CHK AddressingMode DataRegister
+    | CLR Size AddressingMode
+    | CMP Size AddressingMode DataRegister
+    | CMPA Size AddressingMode AddressRegister
+    | CMPI Size nat AddressingMode
+    | CMPM Size AddressRegister AddressRegister
+    | DBT DataRegister nat
+    | DBF DataRegister nat
+    | DBcc Condition DataRegister nat
+    | DIVS AddressingMode DataRegister
+    | DIVU AddressingMode DataRegister
+    | EOR Size DataRegister AddressingMode
+    | EORI Size nat AddressingMode
+    | EORItoCCR nat
+    | EORItoSR nat
+    | EXG DataOrAddressRegister DataOrAddressRegister
+    | EXT Size DataRegister
+    | ILLEGAL
+    | JMP AddressingMode
+    | JSR AddressingMode
+    | LEA AddressingMode AddressRegister
+    | LINK AddressRegister nat
+    | LSL Size AddressingMode DataRegister
+    | LSLW AddressingMode
+    | LSR Size AddressingMode DataRegister
+    | LSRW AddressingMode
+    | MOVE Size AddressingMode AddressingMode
+    | MOVEtoCCR AddressingMode
+    | MOVEtoSR AddressingMode
+    | MOVEfromSR AddressingMode
+    | MOVEtoUSP AddressingMode
+    | MOVEfromUSP AddressingMode
+    | MOVEA Size AddressingMode AddressRegister
+    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
+    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
+    | MOVEP Size AddressingMode AddressingMode
+    | MOVEQ nat DataRegister
+    | MULS AddressingMode DataRegister
+    | MULU AddressingMode DataRegister
+    | NBCD AddressingMode
+    | NEG Size AddressingMode
+    | NEGX Size AddressingMode
+    | NOP
+    | NOT Size AddressingMode
+    | OR Size AddressingMode AddressingMode
+    | ORI Size nat AddressingMode
+    | ORItoCCR nat
+    | ORItoSR nat
+    | PEA AddressingMode
+    | RESET
+    | ROL Size AddressingMode DataRegister
+    | ROLW AddressingMode
+    | ROR Size AddressingMode DataRegister
+    | RORW AddressingMode
+    | ROXL Size AddressingMode DataRegister
+    | ROXLW AddressingMode
+    | ROXR Size AddressingMode DataRegister
+    | ROXRW AddressingMode
+    | RTE
+    | RTR
+    | RTS
+    | SBCD AddressingMode AddressingMode
+    | ST AddressingMode
+    | SF AddressingMode
+    | Scc Condition AddressingMode
+    | STOP nat
+    | SUB Size AddressingMode AddressingMode
+    | SUBA Size AddressingMode AddressingMode
+    | SUBI Size nat AddressingMode
+    | SUBQ Size nat AddressingMode
+    | SUBX Size AddressingMode AddressingMode
+    | SWAP DataRegister
+    | TAS AddressingMode
+    | TRAP nat
+    | TRAPV
+    | TST Size AddressingMode
+    | UNLK AddressRegister
+
+end
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Datatype_Benchmark/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/ROOT.ML	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,8 @@
+(*  Title:      HOL/Datatype_Benchmark/ROOT.ML
+
+Some rather large datatype examples (from John Harrison).
+*)
+
+Toplevel.timing := true;
+
+use_thys ["Brackin", "Instructions", "SML", "Verilog"];
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Datatype_Benchmark/SML.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/SML.thy	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,91 @@
+(*  Title:      HOL/Datatype_Benchmark/SML.thy
+
+Example from Myra: part of the syntax of SML.
+*)
+
+theory SML imports Main begin
+
+datatype
+  string = EMPTY_STRING | CONS_STRING nat string
+
+datatype
+   strid = STRID string
+
+datatype
+   var = VAR string
+
+datatype
+   con = CON string
+
+datatype
+   scon = SCINT nat | SCSTR string
+
+datatype
+   excon = EXCON string
+
+datatype
+   label = LABEL string
+
+datatype
+  'a nonemptylist = Head_and_tail 'a "'a list"
+
+datatype
+  'a long = BASE 'a | QUALIFIED strid "'a long"
+
+datatype
+   atpat_e = WILDCARDatpat_e
+           | SCONatpat_e scon
+           | VARatpat_e var
+           | CONatpat_e "con long"
+           | EXCONatpat_e "excon long"
+           | RECORDatpat_e "patrow_e option"
+           | PARatpat_e pat_e
+and
+   patrow_e = DOTDOTDOT_e
+            | PATROW_e label pat_e "patrow_e option"
+and
+   pat_e = ATPATpat_e atpat_e
+         | CONpat_e "con long" atpat_e
+         | EXCONpat_e "excon long" atpat_e
+         | LAYEREDpat_e var pat_e
+and
+   conbind_e = CONBIND_e con "conbind_e option"
+and
+   datbind_e = DATBIND_e conbind_e "datbind_e option"
+and
+   exbind_e = EXBIND1_e excon "exbind_e option"
+            | EXBIND2_e excon "excon long" "exbind_e option"
+and
+   atexp_e = SCONatexp_e scon
+           | VARatexp_e "var long"
+           | CONatexp_e "con long"
+           | EXCONatexp_e "excon long"
+           | RECORDatexp_e "exprow_e option"
+           | LETatexp_e dec_e exp_e
+           | PARatexp_e exp_e
+and
+   exprow_e = EXPROW_e label exp_e "exprow_e option"
+and
+   exp_e = ATEXPexp_e atexp_e
+         | APPexp_e exp_e atexp_e
+         | HANDLEexp_e exp_e match_e
+         | RAISEexp_e exp_e
+         | FNexp_e match_e
+and
+   match_e = MATCH_e mrule_e "match_e option"
+and
+   mrule_e = MRULE_e pat_e exp_e
+and
+   dec_e = VALdec_e valbind_e
+         | DATATYPEdec_e datbind_e
+         | ABSTYPEdec_e datbind_e dec_e
+         | EXCEPTdec_e exbind_e
+         | LOCALdec_e dec_e dec_e
+         | OPENdec_e "strid long nonemptylist"
+         | EMPTYdec_e
+         | SEQdec_e dec_e dec_e
+and
+   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
+             | RECvalbind_e valbind_e
+
+end
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Datatype_Benchmark/Verilog.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/Verilog.thy	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,138 @@
+(*  Title:      HOL/Datatype_Benchmark/Verilog.thy
+
+Example from Daryl: a Verilog grammar.
+*)
+
+theory Verilog imports Main begin
+
+datatype
+  Source_text
+     = module string "string list" "Module_item list"
+     | Source_textMeta string
+and
+  Module_item
+     = "declaration" Declaration
+     | initial Statement
+     | always Statement
+     | assign Lvalue Expression
+     | Module_itemMeta string
+and
+  Declaration
+     = reg_declaration "Range option" "string list"
+     | net_declaration "Range option" "string list"
+     | input_declaration "Range option" "string list"
+     | output_declaration "Range option" "string list"
+     | DeclarationMeta string
+and
+  Range = range Expression Expression | RangeMeta string
+and
+  Statement
+     = clock_statement Clock Statement_or_null
+     | blocking_assignment Lvalue Expression
+     | non_blocking_assignment Lvalue Expression
+     | conditional_statement
+          Expression Statement_or_null "Statement_or_null option"
+     | case_statement Expression "Case_item list"
+     | while_loop Expression Statement
+     | repeat_loop Expression Statement
+     | for_loop
+          Lvalue Expression Expression Lvalue Expression Statement
+     | forever_loop Statement
+     | disable string
+     | seq_block "string option" "Statement list"
+     | StatementMeta string
+and
+  Statement_or_null
+     = statement Statement | null_statement | Statement_or_nullMeta string
+and
+  Clock
+     = posedge string
+     | negedge string
+     | clock string
+     | ClockMeta string
+and
+  Case_item
+     = case_item "Expression list" Statement_or_null
+     | default_case_item Statement_or_null
+     | Case_itemMeta string
+and
+  Expression
+     = plus Expression Expression
+     | minus Expression Expression
+     | lshift Expression Expression
+     | rshift Expression Expression
+     | lt Expression Expression
+     | leq Expression Expression
+     | gt Expression Expression
+     | geq Expression Expression
+     | logeq Expression Expression
+     | logneq Expression Expression
+     | caseeq Expression Expression
+     | caseneq Expression Expression
+     | bitand Expression Expression
+     | bitxor Expression Expression
+     | bitor Expression Expression
+     | logand Expression Expression
+     | logor Expression Expression
+     | conditional Expression Expression Expression
+     | positive Primary
+     | negative Primary
+     | lognot Primary
+     | bitnot Primary
+     | reducand Primary
+     | reducxor Primary
+     | reducor Primary
+     | reducnand Primary
+     | reducxnor Primary
+     | reducnor Primary
+     | primary Primary
+     | ExpressionMeta string
+and
+  Primary
+     = primary_number Number
+     | primary_IDENTIFIER string
+     | primary_bit_select string Expression
+     | primary_part_select string Expression Expression
+     | primary_gen_bit_select Expression Expression
+     | primary_gen_part_select Expression Expression Expression
+     | primary_concatenation Concatenation
+     | primary_multiple_concatenation Multiple_concatenation
+     | brackets Expression
+     | PrimaryMeta string
+and
+  Lvalue
+     = lvalue string
+     | lvalue_bit_select string Expression
+     | lvalue_part_select string Expression Expression
+     | lvalue_concatenation Concatenation
+     | LvalueMeta string
+and
+  Number
+     = decimal string
+     | based "string option" string
+     | NumberMeta string
+and
+  Concatenation
+     = concatenation "Expression list" | ConcatenationMeta string
+and
+  Multiple_concatenation
+     = multiple_concatenation Expression "Expression list"
+     | Multiple_concatenationMeta string
+and
+  meta
+     = Meta_Source_text Source_text
+     | Meta_Module_item Module_item
+     | Meta_Declaration Declaration
+     | Meta_Range Range
+     | Meta_Statement Statement
+     | Meta_Statement_or_null Statement_or_null
+     | Meta_Clock Clock
+     | Meta_Case_item Case_item
+     | Meta_Expression Expression
+     | Meta_Primary Primary
+     | Meta_Lvalue Lvalue
+     | Meta_Number Number
+     | Meta_Concatenation Concatenation
+     | Meta_Multiple_concatenation Multiple_concatenation
+
+end
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/HOLCF/IsaMakefile
--- a/src/HOL/HOLCF/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/HOL/HOLCF/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -17,6 +17,7 @@
   IOA-Storage \
   IOA-ex
 all: images test
+full: all
 
 
 ## global settings
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -81,6 +81,10 @@
   HOL-ZF
     # ^ this is the sort position
 
+benchmark: \
+  HOL-Datatype_Benchmark \
+  HOL-Record_Benchmark
+
 images-no-smlnj: \
   HOL-Probability
 
@@ -91,8 +95,10 @@
   HOL-Nominal-Examples
 
 all: test-no-smlnj test images-no-smlnj images
+full: all benchmark
 smlnj: test images
 
+
 ## global settings
 
 SRC = $(ISABELLE_HOME)/src
@@ -1772,6 +1778,28 @@
 	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
 
 
+
+## HOL-Datatype_Benchmark
+
+HOL-Datatype_Benchmark: HOL $(LOG)/HOL-Datatype_Benchmark.gz
+
+$(LOG)/HOL-Datatype_Benchmark.gz: $(OUT)/HOL				\
+  Datatype_Benchmark/ROOT.ML Datatype_Benchmark/Brackin.thy		\
+  Datatype_Benchmark/Instructions.thy Datatype_Benchmark/SML.thy	\
+  Datatype_Benchmark/Verilog.thy
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Datatype_Benchmark
+
+
+## HOL-Record_Benchmark
+
+HOL-Record_Benchmark: HOL $(LOG)/HOL-Record_Benchmark.gz
+
+$(LOG)/HOL-Record_Benchmark.gz: $(OUT)/HOL Record_Benchmark/ROOT.ML	\
+   Record_Benchmark/Record_Benchmark.thy
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark
+
+
+
 ## clean
 
 clean:
@@ -1799,23 +1827,25 @@
 		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz		\
 		$(LOG)/HOL-Proofs-Extraction.gz				\
 		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
-		$(LOG)/HOL-Word-SMT_Examples.gz				\
-		$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz	\
-		$(LOG)/HOL-SPARK-Manual.gz				\
-		$(LOG)/HOL-Statespace.gz				\
+		$(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz	\
+		$(LOG)/HOL-SPARK-Examples.gz				\
+		$(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz	\
 		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
 		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
 		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\
 		$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
 		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
 		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
-		$(OUT)/HOL-IMP $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
-		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
+		$(OUT)/HOL-IMP $(OUT)/HOL-Main				\
+		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
+		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain			\
 		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
-		$(OUT)/HOL-SPARK					\
-		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA			\
-		$(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
-		$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
-		$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
+		$(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/HOL4		\
+		$(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz			\
+		$(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz			\
+		$(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz		\
+		$(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz			\
 		$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz		\
-		$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
+		$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz		\
+		$(LOG)/HOL-Datatype_Benchmark.gz			\
+		$(LOG)/HOL-Record_Benchmark.gz
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 14 15:50:15 2011 +0100
@@ -6,7 +6,8 @@
 
 signature NOMINAL_DATATYPE =
 sig
-  val add_nominal_datatype : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
+  val nominal_datatype : Datatype.config -> Datatype.spec list -> theory -> theory
+  val nominal_datatype_cmd : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
   type descr
   type nominal_datatype_info
   val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -185,7 +186,7 @@
 fun fresh_star_const T U =
   Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
-fun gen_add_nominal_datatype prep_specs config dts thy =
+fun gen_nominal_datatype prep_specs config dts thy =
   let
     val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;
 
@@ -2065,11 +2066,12 @@
     thy13
   end;
 
-val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_specs;
+val nominal_datatype = gen_nominal_datatype Datatype.check_specs;
+val nominal_datatype_cmd = gen_nominal_datatype Datatype.read_specs;
 
 val _ =
-  Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
-    (Parse.and_list1 Datatype.spec_cmd
-      >> (Toplevel.theory o add_nominal_datatype Datatype.default_config));
+  Outer_Syntax.command "nominal_datatype" "define nominal datatypes" Keyword.thy_decl
+    (Parse.and_list1 Datatype.spec_cmd >>
+      (Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
 
 end
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Record_Benchmark/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Record_Benchmark/ROOT.ML	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,8 @@
+(*  Title:      HOL/Record_Benchmark/ROOT.ML
+
+Some benchmark on large record.
+*)
+
+Toplevel.timing := true;
+
+use_thys ["Record_Benchmark"];
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Record_Benchmark/Record_Benchmark.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy	Wed Dec 14 15:50:15 2011 +0100
@@ -0,0 +1,390 @@
+(*  Title:      HOL/Record_Benchmark/Record_Benchmark.thy
+    Author:     Norbert Schirmer, DFKI
+*)
+
+header {* Benchmark for large record *}
+
+theory Record_Benchmark
+imports Main
+begin
+
+declare [[record_timing]]
+
+record many_A =
+A000::nat
+A001::nat
+A002::nat
+A003::nat
+A004::nat
+A005::nat
+A006::nat
+A007::nat
+A008::nat
+A009::nat
+A010::nat
+A011::nat
+A012::nat
+A013::nat
+A014::nat
+A015::nat
+A016::nat
+A017::nat
+A018::nat
+A019::nat
+A020::nat
+A021::nat
+A022::nat
+A023::nat
+A024::nat
+A025::nat
+A026::nat
+A027::nat
+A028::nat
+A029::nat
+A030::nat
+A031::nat
+A032::nat
+A033::nat
+A034::nat
+A035::nat
+A036::nat
+A037::nat
+A038::nat
+A039::nat
+A040::nat
+A041::nat
+A042::nat
+A043::nat
+A044::nat
+A045::nat
+A046::nat
+A047::nat
+A048::nat
+A049::nat
+A050::nat
+A051::nat
+A052::nat
+A053::nat
+A054::nat
+A055::nat
+A056::nat
+A057::nat
+A058::nat
+A059::nat
+A060::nat
+A061::nat
+A062::nat
+A063::nat
+A064::nat
+A065::nat
+A066::nat
+A067::nat
+A068::nat
+A069::nat
+A070::nat
+A071::nat
+A072::nat
+A073::nat
+A074::nat
+A075::nat
+A076::nat
+A077::nat
+A078::nat
+A079::nat
+A080::nat
+A081::nat
+A082::nat
+A083::nat
+A084::nat
+A085::nat
+A086::nat
+A087::nat
+A088::nat
+A089::nat
+A090::nat
+A091::nat
+A092::nat
+A093::nat
+A094::nat
+A095::nat
+A096::nat
+A097::nat
+A098::nat
+A099::nat
+A100::nat
+A101::nat
+A102::nat
+A103::nat
+A104::nat
+A105::nat
+A106::nat
+A107::nat
+A108::nat
+A109::nat
+A110::nat
+A111::nat
+A112::nat
+A113::nat
+A114::nat
+A115::nat
+A116::nat
+A117::nat
+A118::nat
+A119::nat
+A120::nat
+A121::nat
+A122::nat
+A123::nat
+A124::nat
+A125::nat
+A126::nat
+A127::nat
+A128::nat
+A129::nat
+A130::nat
+A131::nat
+A132::nat
+A133::nat
+A134::nat
+A135::nat
+A136::nat
+A137::nat
+A138::nat
+A139::nat
+A140::nat
+A141::nat
+A142::nat
+A143::nat
+A144::nat
+A145::nat
+A146::nat
+A147::nat
+A148::nat
+A149::nat
+A150::nat
+A151::nat
+A152::nat
+A153::nat
+A154::nat
+A155::nat
+A156::nat
+A157::nat
+A158::nat
+A159::nat
+A160::nat
+A161::nat
+A162::nat
+A163::nat
+A164::nat
+A165::nat
+A166::nat
+A167::nat
+A168::nat
+A169::nat
+A170::nat
+A171::nat
+A172::nat
+A173::nat
+A174::nat
+A175::nat
+A176::nat
+A177::nat
+A178::nat
+A179::nat
+A180::nat
+A181::nat
+A182::nat
+A183::nat
+A184::nat
+A185::nat
+A186::nat
+A187::nat
+A188::nat
+A189::nat
+A190::nat
+A191::nat
+A192::nat
+A193::nat
+A194::nat
+A195::nat
+A196::nat
+A197::nat
+A198::nat
+A199::nat
+A200::nat
+A201::nat
+A202::nat
+A203::nat
+A204::nat
+A205::nat
+A206::nat
+A207::nat
+A208::nat
+A209::nat
+A210::nat
+A211::nat
+A212::nat
+A213::nat
+A214::nat
+A215::nat
+A216::nat
+A217::nat
+A218::nat
+A219::nat
+A220::nat
+A221::nat
+A222::nat
+A223::nat
+A224::nat
+A225::nat
+A226::nat
+A227::nat
+A228::nat
+A229::nat
+A230::nat
+A231::nat
+A232::nat
+A233::nat
+A234::nat
+A235::nat
+A236::nat
+A237::nat
+A238::nat
+A239::nat
+A240::nat
+A241::nat
+A242::nat
+A243::nat
+A244::nat
+A245::nat
+A246::nat
+A247::nat
+A248::nat
+A249::nat
+A250::nat
+A251::nat
+A252::nat
+A253::nat
+A254::nat
+A255::nat
+A256::nat
+A257::nat
+A258::nat
+A259::nat
+A260::nat
+A261::nat
+A262::nat
+A263::nat
+A264::nat
+A265::nat
+A266::nat
+A267::nat
+A268::nat
+A269::nat
+A270::nat
+A271::nat
+A272::nat
+A273::nat
+A274::nat
+A275::nat
+A276::nat
+A277::nat
+A278::nat
+A279::nat
+A280::nat
+A281::nat
+A282::nat
+A283::nat
+A284::nat
+A285::nat
+A286::nat
+A287::nat
+A288::nat
+A289::nat
+A290::nat
+A291::nat
+A292::nat
+A293::nat
+A294::nat
+A295::nat
+A296::nat
+A297::nat
+A298::nat
+A299::nat
+
+lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
+  by simp
+
+lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
+  by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+  by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
+  done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+  apply simp
+  done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply simp
+  done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+  apply simp
+  done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply simp
+  done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+  apply auto
+  done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply auto
+  done
+
+lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply auto
+  done
+
+lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+  apply auto
+  done
+
+
+lemma True
+proof -
+  {
+    fix P r
+    assume pre: "P (A155 r)"
+    have "\<exists>x. P x"
+      using pre
+      apply -
+      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+      apply auto 
+      done
+  }
+  show ?thesis ..
+qed
+
+
+lemma "\<exists>r. A155 r = x"
+  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
+  done
+
+
+end
\ No newline at end of file
diff -r a8b9191609a8 -r 7887eabb1997 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Dec 14 15:50:15 2011 +0100
@@ -19,7 +19,7 @@
   val read_specs: spec_cmd list -> theory -> spec list * Proof.context
   val check_specs: spec list -> theory -> spec list * Proof.context
   val add_datatype: config -> spec list -> theory -> string list * theory
-  val add_datatype_cmd: spec_cmd list -> theory -> theory
+  val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory
   val spec_cmd: spec_cmd parser
 end;
 
@@ -798,7 +798,7 @@
   end;
 
 val add_datatype = gen_add_datatype check_specs;
-val add_datatype_cmd = snd oo gen_add_datatype read_specs Datatype_Aux.default_config;
+val add_datatype_cmd = gen_add_datatype read_specs;
 
 
 (* outer syntax *)
@@ -810,7 +810,8 @@
 
 val _ =
   Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
-    (Parse.and_list1 spec_cmd >> (Toplevel.theory o add_datatype_cmd));
+    (Parse.and_list1 spec_cmd
+      >> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config)));
 
 
 open Datatype_Data;
diff -r a8b9191609a8 -r 7887eabb1997 src/LCF/IsaMakefile
--- a/src/LCF/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/LCF/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: LCF
 test: LCF-ex
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/Pure/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: Pure
 test: RAW
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/Sequents/IsaMakefile
--- a/src/Sequents/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/Sequents/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -8,6 +8,7 @@
 images: Sequents
 test: Sequents-LK
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/Tools/WWW_Find/IsaMakefile
--- a/src/Tools/WWW_Find/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/Tools/WWW_Find/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -9,6 +9,7 @@
 images:
 test: Pure-WWW_Find
 all: images test
+full: all
 smlnj: all
 
 
diff -r a8b9191609a8 -r 7887eabb1997 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/Tools/misc_legacy.ML	Wed Dec 14 15:50:15 2011 +0100
@@ -22,7 +22,6 @@
   val term_frees: term -> term list
   val mk_defpair: term * term -> string * term
   val get_def: theory -> xstring -> thm
-  val simple_read_term: theory -> typ -> string -> term
   val METAHYPS: (thm list -> tactic) -> int -> tactic
 end;
 
@@ -104,15 +103,6 @@
 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 
 
-fun simple_read_term thy T s =
-  let
-    val ctxt = Proof_Context.init_global thy
-      |> Proof_Context.allow_dummies
-      |> Proof_Context.set_mode Proof_Context.mode_schematic;
-    val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
-  in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
-
-
 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
        METAHYPS (fn prems => tac prems) i
 
diff -r a8b9191609a8 -r 7887eabb1997 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed Dec 14 15:05:22 2011 +0100
+++ b/src/ZF/IsaMakefile	Wed Dec 14 15:50:15 2011 +0100
@@ -10,6 +10,7 @@
 #Note: keep targets sorted
 test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
 all: images test
+full: all
 smlnj: all