StackRating

An Elo-based rating system for Stack Overflow
Home   |   About   |   Stats and Analysis   |   Get a Badge
Rating Stats for

Andreas Lochbihler

Rating
1576.77 (3,311th) 		Reputation
4,488 (37,143rd)
Page: 1 2 3
Title Δ
Isabelle use Locale or Context outside of any locale 0.00
Can isabelle unfold definitions with explicit type? 0.00
How do I code algebraic cpos as an Isabelle locale 0.00
{0,1} as function type in Isabelle 0.00
Conditional definition in Isabelle 0.00
How to use a definition written on locale parameters in the assumpt... 0.00
Datatype transformation function takes very long to proof 0.00
Shorten proposition with abbreviations in Isabelle 0.00
How to simplify an inductive predicate by evaluation? 0.00
How to generate code for the existential quantifier +0.39
Isabelle: How can I position fixed arguments in mixfix notation? +0.39
Proving the set of reachable states of semantics function is finite... 0.00
How to generate code for less_eq operation 0.00
An inductive predicate enumerating set elements 0.00
Proving associativity of sequential composition in Isabelle 0.00
operation of elements in a set in Isabelle 0.00
Can erule produce erroneous subgoals? 0.00
How can I fake existential types in Isabelle/HOL? 0.00
Problems with termination of a recursive function using zip, map, a... 0.00
Instantiating axioms about Sequents explicitly 0.00
Applying axioms about Sequents 0.00
Isabelle/HOL: access interpretation in another locale 0.00
Isabelle/HOL: What does the THE construct denote? 0.00
How can I tell simp to instantiate schematic variables? +0.40
quotient_type warning "no map function" 0.00
What support does Isabelle have for relations represented by binary... 0.00
Isabelle: Wellsortedness error 0.00
How to do an inductive definition over "booleans" in Isab... 0.00
How can I efficiently prove existential propositions with multiple... +3.23
Print/query class instances in Isabelle 0.00
Is there an additive version of "Power.thy" in Isabelle? +3.21
How to define an abstract collection data type? 0.00
How to define Sup for an inductive datatype? 0.00
Reordering goals (Isabelle) 0.00
How to define an inductive predicate inside locale? 0.00
How to find constructors of a datatype? +3.55
How to use complex patterns in functions? 0.00
How to define a supremum on a set? 0.00
"Efficient" least- and greatest fixpoint computations? 0.00
Is there anything like a subst_tac rule in Isabelle? 0.00
How to use classes or locales? 0.00
How to use code_pred and values? 0.00
Mutual recursion in primcofix 0.00
Isabelle HOLCF doesn't understand fixrec 0.00
Free type variables in proof by induction +3.21
Renaming the schematic variables 0.00
The order of premises 0.00
Simplify meta-universally quantified assumptions with equality 0.00
What is (*>*) in Isabelle? 0.00
Conditional rewrite rules with unknowns in condition +3.34