# HG changeset patch # User wenzelm # Date 1159479782 -7200 # Node ID 5855d1bbf2103816f288cf11d916f75468af40c9 # Parent 4eb07237382a1a238463626f49a740e12f7bfc1a obsolete; diff -r 4eb07237382a -r 5855d1bbf210 src/HOL/Isar_examples/Cantor.ML --- a/src/HOL/Isar_examples/Cantor.ML Thu Sep 28 23:43:00 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ - -(* tactic script -- single steps *) - -Goal "EX S. S ~: range (f :: 'a => 'a set)"; - by (rtac exI 1); - by (rtac notI 1); - by (etac rangeE 1); - by (etac equalityCE 1); - by (dtac CollectD 1); - by (contr_tac 1); - by (swap_res_tac [CollectI] 1); - by (assume_tac 1); -qed ""; - - -(* tactic script -- automatic *) - -Goal "EX S. S ~: range (f :: 'a => 'a set)"; - by (Best_tac 1); -qed ""; diff -r 4eb07237382a -r 5855d1bbf210 src/HOL/Real/document/root.tex --- a/src/HOL/Real/document/root.tex Thu Sep 28 23:43:00 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ - -% $Id$ - -\documentclass[11pt,a4paper]{article} -\usepackage{graphicx,isabelle,isabellesym,latexsym} -\usepackage[latin1]{inputenc} -\usepackage{pdfsetup} - -\urlstyle{rm} -\isabellestyle{it} - -\begin{document} - -\title{Isabelle/HOL-Real --- Higher-Order Logic with Real Numbers} -\maketitle - -\tableofcontents - -\parindent 0pt\parskip 0.5ex -\input{session} - -\end{document} diff -r 4eb07237382a -r 5855d1bbf210 src/HOLCF/HOLCF.ML --- a/src/HOLCF/HOLCF.ML Thu Sep 28 23:43:00 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOLCF/HOLCF.ML - ID: $Id$ -*) - -structure HOLCF = -struct - val thy = the_context (); -end;