- Mar 20, 2016
-
-
Lars Hupel authored
-
Lars Hupel authored
Notable changes: * sbt-libisabelle plugin which takes care of Isabelle source management - no more submodules; Isabelle sources are now packaged in JAR files - no weird ROOTS file in the repository root * less isabelle: flags, everybody would want to use the defaults anyway * updating to Isabelle2016 becomes possible (future work)
-
- Mar 17, 2016
-
-
Regis Blanc authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Regis Blanc authored
-
Regis Blanc authored
-
Regis Blanc authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
Use a LetPattern Also reenable printing of LetPattern
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
simplify terminatingCalls
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
terminatingCalls now returns calls with integers too. IntInduction and all integer comparison rules are phased out. Instead there is a single InequalitySplit rules which splits into (up to) 3 branches, taking pc into account. No more EqualitySplit for any other type, except generic types. Isolate unused rules. Clean up Rules. Improve QualifiedExamplesBank API
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
Manos Koukoutos authored
Use Grammars.default Remove SafeRecursiveCalls
-