author | wenzelm |
Tue, 18 Mar 2008 22:19:18 +0100 | |
changeset 26322 | eaf634e975fa |
parent 25991 | 31b38a39e589 |
child 26408 | 6964c4799f47 |
permissions | -rw-r--r-- |
(* Title: FOLP/ex/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Examples for First-Order Logic. *) use_thys [ "Intro", "Nat", "Foundation", "If", "Intuitionistic", "Classical" ]; val thy = theory "IFOLP" and tac = IntPr.fast_tac 1; time_use "prop.ML"; time_use "quant.ML"; val thy = theory "FOLP" and tac = Cla.fast_tac FOLP_cs 1; time_use "prop.ML"; time_use "quant.ML";