Nuprl 4.2 Standard Theories

• boot
• core_1
• rules_1
• rules_2
• ml_1
• core_2
• well_fnd
• int_1
• bool_1
• union
• fun_1
• rel_1
• subtyping
• quot_1
• int_2
• list_1
• num_thy_1

Doug Howe's representation of HOL basic theories in Nuprl 4.2

• min
• bool
• restr_binder
• combin
• sum
• one
• num
• pair
• BASIC_HOL
• prim_rec
• arithmetic
• list
• recursive_types
• tree
• ltree
• rec_type
• HOL
• operator
• List
• cl
• mil
• norm
• norma
• normd
• HOL_simps

Representation of Isabelle theories in Nuprl

• Auxilary Nuprl theory port
• Arith Theory
  • Original Isabelle version
  • Nuprl image