Page MenuHomeIsabelle/Phabricator

florian.haftmann (Florian Haftmann)
User

Projects

User Details

User Since
Nov 30 2019, 9:26 AM (26 w, 3 d)

Recent Activity

Sat, May 30

florian.haftmann committed rISABELLE435cdc772110: specific atomization inert to later rule set modifications.
specific atomization inert to later rule set modifications
Sat, May 30, 8:07 PM
florian.haftmann committed rISABELLE3956d85e8e81: more precise scope of atomize.
more precise scope of atomize
Sat, May 30, 8:07 PM
florian.haftmann committed rISABELLE3867734b9a40: install simproc but deactivate by default.
install simproc but deactivate by default
Sat, May 30, 1:49 PM

Mon, May 25

florian.haftmann committed rISABELLE4f4695757980: better closeup and more consistent terminology.
better closeup and more consistent terminology
Mon, May 25, 7:45 AM

Fri, May 22

florian.haftmann committed rISABELLE6a51e64ba13d: slightly more specific implementations.
slightly more specific implementations
Fri, May 22, 6:29 AM
florian.haftmann committed rISABELLE30d92e668b52: tuned module name space for generated code.
tuned module name space for generated code
Fri, May 22, 6:29 AM

Thu, May 21

florian.haftmann committed rISABELLE34ecb540a079: generalized and augmented.
generalized and augmented
Thu, May 21, 11:04 AM

Wed, May 20

florian.haftmann committed rISABELLEda12452c9be2: corrected spelling and tuned whitespace.
corrected spelling and tuned whitespace
Wed, May 20, 8:35 AM

Sat, May 9

florian.haftmann committed rISABELLEf424e164d752: modernized notation for bit operations.
modernized notation for bit operations
Sat, May 9, 7:34 PM
florian.haftmann committed rAFPe3d9183d726a: modernized notation for bit operations.
modernized notation for bit operations
Sat, May 9, 7:33 PM

Fri, May 8

florian.haftmann committed rISABELLE214b48a1937b: explicit mask operation for bits.
explicit mask operation for bits
Fri, May 8, 8:36 AM
florian.haftmann committed rISABELLE67cc2319104f: prefer _ mod 2 over of_bool (odd _).
prefer _ mod 2 over of_bool (odd _)
Fri, May 8, 8:36 AM
florian.haftmann committed rISABELLE541e68d1a964: less aggressive default simp rules.
less aggressive default simp rules
Fri, May 8, 8:36 AM

Apr 27 2020

florian.haftmann committed rISABELLE6fd70ed18199: simplified construction of binary bit operations.
simplified construction of binary bit operations
Apr 27 2020, 6:30 PM

Apr 26 2020

florian.haftmann committed rISABELLE14914ae80f70: temporarily revert change which does not work as expected.
temporarily revert change which does not work as expected
Apr 26 2020, 7:06 AM
florian.haftmann committed rISABELLEab3cecb836b5: more rules.
more rules
Apr 26 2020, 7:06 AM

Apr 25 2020

florian.haftmann committed rISABELLE35a951ed2e82: documentation of relevant ideas.
documentation of relevant ideas
Apr 25 2020, 6:44 AM
florian.haftmann committed rISABELLEe00712b4e2c2: numeral rules for take_bit / drop_bit on int.
numeral rules for take_bit / drop_bit on int
Apr 25 2020, 6:44 AM
florian.haftmann committed rISABELLEfc4f9dad5292: opaque export does not work as expected in presence of dependent instances.
opaque export does not work as expected in presence of dependent instances
Apr 25 2020, 6:44 AM

Apr 22 2020

florian.haftmann committed rISABELLEca3ac5238c41: hooks for foundational terms: protection of foundational terms during….
hooks for foundational terms: protection of foundational terms during…
Apr 22 2020, 8:38 PM

Apr 20 2020

florian.haftmann committed rISABELLE7c2f4dd48fb6: more robust judgment handling.
more robust judgment handling
Apr 20 2020, 9:11 AM

Apr 16 2020

florian.haftmann committed rISABELLEe4e05fcd8937: generalized.
generalized
Apr 16 2020, 12:48 PM
florian.haftmann committed rISABELLE816e52bbfa60: more theorems.
more theorems
Apr 16 2020, 12:48 PM
florian.haftmann committed rISABELLE02c50bba9304: bit on numerals.
bit on numerals
Apr 16 2020, 12:48 PM
florian.haftmann committed rISABELLE2e3fa4e7cd73: another rule on numerals.
another rule on numerals
Apr 16 2020, 12:48 PM
florian.haftmann committed rISABELLE3d1f72d25fc3: more complete rules on numerals.
more complete rules on numerals
Apr 16 2020, 12:48 PM
florian.haftmann committed rISABELLE318695613bb7: more complete rules on numerals.
more complete rules on numerals
Apr 16 2020, 12:48 PM

Mar 9 2020

florian.haftmann committed rISABELLEb612edee9b0c: more frugal simp rules for bit operations; more pervasive use of bit selector.
more frugal simp rules for bit operations; more pervasive use of bit selector
Mar 9 2020, 10:26 PM

Mar 4 2020

florian.haftmann committed rISABELLEbae868febc53: library theory for extractions of equations x = t into premises.
library theory for extractions of equations x = t into premises
Mar 4 2020, 7:37 PM
florian.haftmann committed rISABELLE7807d828a061: tuned.
tuned
Mar 4 2020, 7:37 PM

Mar 3 2020

florian.haftmann committed rISABELLEfe93a863d946: infrastructure for extraction of equations x = t from premises beneath meta-all.
infrastructure for extraction of equations x = t from premises beneath meta-all
Mar 3 2020, 7:36 PM

Feb 13 2020

florian.haftmann committed rISABELLEff6394cfc05c: canonical approach towards lifting.
canonical approach towards lifting
Feb 13 2020, 8:42 AM
florian.haftmann committed rISABELLEd45495e897f4: more instances.
more instances
Feb 13 2020, 8:42 AM
florian.haftmann committed rISABELLE4e66867fd63f: tuned proof.
tuned proof
Feb 13 2020, 8:42 AM

Feb 10 2020

florian.haftmann committed rISABELLE745e518d3d0b: easy abstraction over pointwise bit operations.
easy abstraction over pointwise bit operations
Feb 10 2020, 8:20 AM
florian.haftmann committed rISABELLEf2da99316b86: more rules for natural deduction from inequalities.
more rules for natural deduction from inequalities
Feb 10 2020, 8:20 AM

Feb 9 2020

florian.haftmann committed rISABELLEe83fe2c31088: rule concerning bit (push_bit ...).
rule concerning bit (push_bit ...)
Feb 9 2020, 2:42 PM
florian.haftmann committed rISABELLE7ae4dcf332ae: more lemmas.
more lemmas
Feb 9 2020, 2:42 PM

Feb 5 2020

florian.haftmann committed rISABELLE572ab9e64e18: simplified logical constructions.
simplified logical constructions
Feb 5 2020, 11:18 PM
florian.haftmann committed rISABELLE1d8e914e04d6: simplified logical constructions.
simplified logical constructions
Feb 5 2020, 11:18 PM

Feb 4 2020

florian.haftmann committed rISABELLEbd9d27ccb3a3: more theorems.
more theorems
Feb 4 2020, 7:08 PM

Feb 2 2020

florian.haftmann committed rISABELLE65ffe9e910d4: more specific class assumptions.
more specific class assumptions
Feb 2 2020, 11:27 AM
florian.haftmann committed rISABELLE96d126844adc: more theorems.
more theorems
Feb 2 2020, 11:27 AM

Jan 28 2020

florian.haftmann committed rISABELLE0bb0cb558bf9: sketches of ideas still to come.
sketches of ideas still to come
Jan 28 2020, 8:04 AM
florian.haftmann committed rISABELLE554385d4cf59: more theorems.
more theorems
Jan 28 2020, 8:04 AM
florian.haftmann committed rISABELLE2525e28e4b8b: generalized.
generalized
Jan 28 2020, 8:04 AM
florian.haftmann committed rISABELLE3887432720a9: tuned.
tuned
Jan 28 2020, 8:04 AM

Jan 23 2020

florian.haftmann committed rISABELLE43c2355648d2: tuned.
tuned
Jan 23 2020, 8:40 AM
florian.haftmann committed rISABELLEfb9edfe035e1: tuned.
tuned
Jan 23 2020, 8:40 AM
florian.haftmann committed rISABELLEa3ae93ed7b1b: dropped dead code.
dropped dead code
Jan 23 2020, 8:40 AM