There are few Tutorials about Isabell. There are a few pdf's in Isabelle itself, but a google search to specific problems is quite impossible.
I tryd for example to create a datatype someB (which is equivalent too bool). I create a variable ex1 of type someB. I just want to assigne the value True to that variable. The following code does not work. Does anyone have an idea why? I am probably doing something fundamentally wrong.
datatype someB = "bool"
ex1 :: someB where "ex1 ≡ True"
Type unification failed: Clash of types "bool" and "someB"
Type error in application: incompatible operand type
Operator: op ≡ ex1 :: someB ⇒ prop
Operand: True :: bool