# User Details

User Details

- User Since
- Nov 30 2019, 9:26 AM (43 w, 4 d)

# Fri, Sep 25

Fri, Sep 25

factored out typedef material

factored out typedef material

# Wed, Sep 23

Wed, Sep 23

canonical enum instance for word

florian.haftmann committed rAFPc5f056d78406: more thorough treatment of division, particularly signed division on int and….

more thorough treatment of division, particularly signed division on int and…

florian.haftmann committed rISABELLEbeeadb35e357: more thorough treatment of division, particularly signed division on int and….

more thorough treatment of division, particularly signed division on int and…

canonical enum instance for word

# Sun, Sep 20

Sun, Sep 20

identified operation alias; tuned

# Thu, Sep 17

Thu, Sep 17

NEWS and CONTRIBUTORS

integrated generic conversions into word corpse

integrated generic conversions into word corpse

adjusted to changes in distribution

# Tue, Sep 8

Tue, Sep 8

tuned theory structure

# Mon, Sep 7

Mon, Sep 7

more on conversions

# Sat, Sep 5

Sat, Sep 5

generalized signed_take_bit

more on conversions

generalized signed_take_bit

more on conversions

# Aug 30 2020

Aug 30 2020

more on conversions

more on conversions

# Aug 24 2020

Aug 24 2020

a proof of concept for generic conversions

a proof of concept for generic conversions

# Aug 22 2020

Aug 22 2020

proper syntax declaration

# Aug 10 2020

Aug 10 2020

florian.haftmann committed rAFP9a9bc053eb71: dedicated symbols for code generation, to pave way for generic conversions from….

dedicated symbols for code generation, to pave way for generic conversions from…

florian.haftmann committed rISABELLE9e5862223442: dedicated symbols for code generation, to pave way for generic conversions from….

dedicated symbols for code generation, to pave way for generic conversions from…

consolidated names

reduced prominence od theory Bits_Int

# Aug 6 2020

Aug 6 2020

tailored towards remaining essence

# Aug 5 2020

Aug 5 2020

florian.haftmann committed rISABELLEa36db1c8238e: separation of reversed bit lists from other material.

separation of reversed bit lists from other material

separation of reversed bit lists from other material

florian.haftmann committed rAFPcac1c67360f3: further refinement of code equations for mask operation.

further refinement of code equations for mask operation

florian.haftmann committed rISABELLE3ec876181527: further refinement of code equations for mask operation.

further refinement of code equations for mask operation

# Aug 4 2020

Aug 4 2020

uniform mask operation

clearer separation of pre-word bit list material

uniform mask operation

clearer separation of pre-word bit list material

repaired document slip

# Aug 1 2020

Aug 1 2020

more consequent transferability

more consequent transferability

# Jul 16 2020

Jul 16 2020

tuned grouping

yet another alias

# Jul 13 2020

Jul 13 2020

concatentation of bit values

concatentation of bit values

florian.haftmann committed rISABELLE759532ef0885: prefer canonically oriented lists of bits and more direct characterizations in….

prefer canonically oriented lists of bits and more direct characterizations in…

more simp rules for concrete numerical values

words added to code generator test

florian.haftmann committed rAFP7b844df07b1c: prefer canonically oriented lists of bits in definitions.

prefer canonically oriented lists of bits in definitions

# Jul 11 2020

Jul 11 2020

a generic horner sum operation

more on single-bit operations

signed_take_bit

# Jul 6 2020

Jul 6 2020

separation of traditional bit operations

separation of traditional bit operations

# Jul 5 2020

Jul 5 2020

factored out auxiliary theory

prefer explicit proof

factored out auxiliary theory

# Jul 3 2020

Jul 3 2020

misc lemma tuning

explicit proofs for bit projections

misc lemma tuning

# Jul 2 2020

Jul 2 2020

activated simproc defined_all

florian.haftmann committed rISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-all.

extraction of equations x = t from premises beneath meta-all

updated documentation

obsolete duplicates

removed superfluous dependency

a small aggiornamento for Z2

factored out ancient numeral representation

factored out ancient numeral representation

moved to Word_Lib

more explicit proofs

# Jun 20 2020

Jun 20 2020

simp rules for conversions

florian.haftmann committed rISABELLEd45f5d4c41bd: more class operations for the sake of efficient generated code.

more class operations for the sake of efficient generated code

florian.haftmann committed rAFP0362f33fb949: more class operations for the sake of efficient generated code.

more class operations for the sake of efficient generated code

# Jun 19 2020

Jun 19 2020

prefer single name

prefer single name

# Jun 18 2020

Jun 18 2020

florian.haftmann committed rAFPd5522275e109: build bit operations on word on library theory on bit operations.

build bit operations on word on library theory on bit operations

more instances for uint types

florian.haftmann committed rAFP25bc16f7e44a: canonical bit shifts for word type, leaving duplicates as they are at the moment.

canonical bit shifts for word type, leaving duplicates as they are at the moment

dropped yet another duplicate

replaced mere alias by input abbreviation

replaced mere alias by abbreviation

florian.haftmann committed rAFP23e6a075730d: replaced operation with weak abstraction by input abbreviation.

replaced operation with weak abstraction by input abbreviation

avoid compound operation

replaced mere alias by input abbreviation

bit operations as distinctive library theory

florian.haftmann committed rISABELLE3e162c63371a: build bit operations on word on library theory on bit operations.

build bit operations on word on library theory on bit operations

tweak for code generation

florian.haftmann committed rISABELLE13bb3f5cdc5b: pragmatically ruled out word types of length zero: a bit string with no bits is….

pragmatically ruled out word types of length zero: a bit string with no bits is…