Function definition in higher-order logic

This publication has 19 references indexed in Scilit:

• A Typed Pattern Calculus
  Information and Computation, 1996
• Non-primitive recursive function definitions
  Published by Springer Nature ,1995
• A mechanically verified verification condition generator
  The Computer Journal, 1995
• LCF examples in HOL
  The Computer Journal, 1995
• The Alf proof editor and its proof engine
  Published by Springer Nature ,1994
• Rippling: A heuristic for guiding inductive proofs
  Artificial Intelligence, 1993
• Term rewriting and beyond — theorem proving in Isabelle
  Formal Aspects of Computing, 1989
• Automating Recursive Type Definitions in Higher Order Logic
  Published by Springer Nature ,1989
• Notes on Logic and Set Theory
  Published by Cambridge University Press (CUP) ,1987
• Compiling pattern matching
  Lecture Notes in Computer Science, 1985