doc-src/TutorialI/Rules/ROOT.ML
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 10956 1db8b894ada0
child 16546 77e7fd18b785
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10341
6eb91805a012 added the $Id:$ line
paulson
parents: 10304
diff changeset
     1
(* ID:         $Id$ *)
10304
a372910d82d6 part of set-up
paulson
parents:
diff changeset
     2
use_thy "Basic";
a372910d82d6 part of set-up
paulson
parents:
diff changeset
     3
use_thy "Blast";
a372910d82d6 part of set-up
paulson
parents:
diff changeset
     4
use_thy "Force";
10847
b35a68ec8892 loads the new theory
paulson
parents: 10341
diff changeset
     5
use_thy "Forward";
10956
1db8b894ada0 new examples theory Rules/Tacticals.thy
paulson
parents: 10847
diff changeset
     6
use_thy "Tacticals";
10304
a372910d82d6 part of set-up
paulson
parents:
diff changeset
     7