--- a/src/HOL/Datatype_Examples/Instructions.thy Tue Sep 16 19:23:37 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: HOL/Datatype_Examples/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
-
-old_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
--- a/src/HOL/Datatype_Examples/SML.thy Tue Sep 16 19:23:37 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: HOL/Datatype_Examples/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"
-
-old_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
--- a/src/HOL/Datatype_Examples/Verilog.thy Tue Sep 16 19:23:37 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title: HOL/Datatype_Examples/Verilog.thy
-
-Example from Daryl: a Verilog grammar.
-*)
-
-theory Verilog imports Main begin
-
-old_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
--- a/src/HOL/ROOT Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/ROOT Tue Sep 16 19:23:37 2014 +0200
@@ -755,10 +755,7 @@
Misc_Primrec
theories [condition = ISABELLE_FULL_TEST, timing]
Brackin
- Instructions
IsaFoR
- SML
- Verilog
session "HOL-Word" (main) in Word = HOL +
options [document_graph]