(* Title: HOL/Nonconservative.thy ID: $Id: Nonconservative.thy,v 1.1 2008/01/14 13:37:34 smaus Exp $ Author: Alexander Schimpf, Jan_Georg Smaus *) theory Nonconservative imports Main begin consts c :: bool axioms define_const_by_variable: "c = x" ML {* val define_const_by_variable = thm "define_const_by_variable"; *} end